A Galois connection between classical and intuitionistic logics. II: Semantics

Sergey A. Melikhov

Published 2015-04-13Version 1

Three classes of models of QHC, the joint logic of problems and propositions, are constructed and analyzed, including a class of sheaf models that is closely related to solutions of some actual mathematical problems (such as solutions of algebraic equations) and combines the familiar Leibniz-Euler-Venn semantics of classical logic with a BHK-type semantics of intuitionistic logic. We also describe a first-order theory T over QHC intended to capture the spirit of the ancient Greek tradition of geometry, as presented in Euclid's "Elements". The ancients observed, in what was presumably a consensus view emerging from an earlier debate, a distinction between problems and postulates vs. theorems and axioms (which can also be inferred from the grammar of Euclid's text) and the logical interdependence between the two realms. T formalizes this in terms of the connectives ! and ? of QHC. The purely classical fragment of T is shown to coincide with Tarski's weak elementary geometry, and the purely intuitionistic one with Beeson's "intuitionistic Tarski geometry".