Tarski's theorem on intuitionistic logic, for polyhedra

DOI10.1016/J.APAL.2017.12.005zbMATH Open1390.03015arXiv1701.05094OpenAlexW2963685352MaRDI QIDQ1706265FDOQ1706265

Authors: Nick Bezhanishvili, Vincenzo Marra, Daniel K. McNeill, Andrea Pedrini 

Publication date: 21 March 2018

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: In 1938, Tarski proved that a formula is not intuitionistically valid if, and only if, it has a counter-model in the Heyting algebra of open sets of some topological space. In fact, Tarski showed that any Euclidean space R^n with n >= 1 suffices, as does e.g. the Cantor space. In particular, intuitionistic logic cannot detect topological dimension in the frame of all open sets of a Euclidean space. By contrast, we consider the lattice of open subpolyhedra of a given compact polyhedron P subseteq R^n, prove that it is a locally finite Heyting subalgebra of the (non-locally-finite) algebra of all open sets of R^n, and show that intuitionistic logic is able to capture the topological dimension of P through the bounded-depth axiom schemata. Further, we show that intuitionistic logic is precisely the logic of formul{ae} valid in all Heyting algebras arising from polyhedra in this manner. Thus, our main theorem reconciles through polyhedral geometry two classical results: topological completeness in the style of Tarski, and Jaskowski's theorem that intuitionistic logic enjoys the finite model property. Several questions of interest remain open. E.g., what is the intermediate logic of all closed triangulable manifolds?

Full work available at URL: https://arxiv.org/abs/1701.05094

Recommendations

• scientific article; zbMATH DE number 218533
• Representability and amalgamation for Heyting polyadic algebras
• scientific article; zbMATH DE number 5896226
• Intermediate logics preserving admissible inference rules of heyting calculus
• Interpolation property for extensions of intuitionistic provability logic
• Intermediate logics and the de Jongh property
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• An open mapping theorem for finitely copresented Esakia spaces
• An algebraic approach to filtrations for superintuitionistic logics

zbMATH Keywords

triangulationpolyhedronintuitionistic logictopological semanticsHeyting algebraPL-topologyfinite model proprty

Mathematics Subject Classification ID

Simplicial sets and complexes in algebraic topology (55U10) (n)-dimensional polytopes (52B11) Frames, locales (06D22) Subsystems of classical logic (including intuitionistic logic) (03B20) Heyting algebras (lattice-theoretic aspects) (06D20)

Cites Work

• Title not available (Why is that?)
• Rings of sets
• Title not available (Why is that?)
• Title not available (Why is that?)
• On closed elements in closure algebras
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Some theorems about the sentential calculi of Lewis and Heyting
• Title not available (Why is that?)
• The algebra of topology
• Handbook of Spatial Logics
• Lectures on polyhedral topology
• Title not available (Why is that?)
• Title not available (Why is that?)
• Propositional Calculus and Realizability
• Title not available (Why is that?)
• Bitopological duality for distributive lattices and Heyting algebras
• Gödel algebras free over finite distributive lattices
• Intuitionistic propositional logic is polynomial-space complete
• Completeness of S4 with respect to the real line: revisited
• On formulas of one variable in intuitionistic propositional calculus
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• Title not available (Why is that?)
• Krull dimension in modal logic
• Title not available (Why is that?)
• An algebraic approach to filtrations for superintuitionistic logics

Cited In (8)

• Monic skeleta, boundaries, Aufhebung, and the meaning of `one-dimensionality'
• The spectrum problem for abelian \(\ell\)-groups and MV-algebras
• The successive dimension, without elegance
• The étendue of a combinatorial space and its dimension
• An open mapping theorem for finitely copresented Esakia spaces
• A Spatial Logic for Simplicial Models
• POLYHEDRAL COMPLETENESS OF INTERMEDIATE LOGICS: THE NERVE CRITERION
• Geometric Model Checking of Continuous Space

This page was built for publication: Tarski's theorem on intuitionistic logic, for polyhedra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1706265)