{
  "id": "1312.2575",
  "version": "v2",
  "published": "2013-12-09T20:51:34.000Z",
  "updated": "2015-04-13T22:36:20.000Z",
  "title": "A Galois connection between classical and intuitionistic logics. I: Syntax",
  "authors": [
    "Sergey A. Melikhov"
  ],
  "comment": "35 pages. Parts of the previous version have grown into two separate preprints: \"... II: Semantics\" and \"Mathematical semantics of intuitionistic logic\" (arXiv:1504.????). What remains has been improved and expanded",
  "categories": [
    "math.LO"
  ],
  "abstract": "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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2013-12-09T20:51:34.000Z",
      "title": "A Galois connection between classical and intuitionistic logics",
      "abstract": "In a 1985 commentary to his collected works, Kolmogoroff remarked that his 1932 paper \"was written in hope that with time, the logic of solution of problems will become a permanent part of the logical curriculum. 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, and sheds new light on the basics of intuitionism: 1) 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. 2) Kolmogoroff's double negation translation of QC into QH extends to an interpretation of QHC in QH that is the identity on QH. 3) Goedel's provability translation of QH into the classical modal logic QS4 extends to an interpretation of QHC in QS4, which is identified with a fragment of QHC. Some models of QHC are constructed, including a sheaf-valued model inspired by dependent type theory, which appears to be of interest even as a model of QH (not to be confused with the well-known open-set-valued sheaf models of QH), since it can be seen as a rather accurate formalization of the BHK interpretation of intuitionistism. The paper is addressed to a general mathematical audience and includes a rather unconventional introduction to intuitionistic logic, featuring (a) a motivation via Hilbert's 24th Problem and Lafont's observation that in classical logic, any two proofs of a given theorem are \"homotopic\"; (b) a derivation of Tarski topological models of QH via a model in \"Venn diagrams\" of a classical first-order theory extracted from the clauses of the BHK interpretation.",
      "comment": "68 pages; Preliminary version",
      "journal": null,
      "doi": null
    },
    {
      "version": "v2",
      "updated": "2015-04-13T22:36:20.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "galois connection",
      "intuitionistic logic",
      "intuitionistic predicate calculus qh",
      "bhk interpretation",
      "classical modal logic qs4 extends"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 35,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2013arXiv1312.2575M"
    }
  }
}