A Galois connection between classical and intuitionistic logics. I: Syntax

Sergey A. Melikhov

Published 2013-12-09, updated 2015-04-13Version 2

In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper "was written in hope that with time, the logic of solution of problems [i.e., intuitionistic logic] will become a permanent part of a [standard] course of logic. Creation of a unified logical apparatus dealing with objects of two types --- propositions and problems --- was intended." We construct such a formal system QHC, which is a conservative extension of both the intuitionistic predicate calculus QH and the classical predicate calculus QC. The only new connectives ? and ! of QHC induce a Galois connection (i.e., a pair of adjoint functors) between the Lindenbaum algebras of QH and QC. Kolmogorov's double negation translation of propositions into problems extends to a retraction of QHC onto QH; whereas Goedel's provability translation of problems into modal propositions extends to a retraction of QHC onto its QC+(?!) fragment, identified with the modal logic QS4. The QH+(!?) fragment is an intuitionistic modal logic whose modality !? is a strict lax modality in the sense of Aczel --- and thus resembles the squash/bracket operation in intuitionistic type theories.