{
  "id": "1504.03379",
  "version": "v1",
  "published": "2015-04-13T22:13:29.000Z",
  "updated": "2015-04-13T22:13:29.000Z",
  "title": "A Galois connection between classical and intuitionistic logics. II: Semantics",
  "authors": [
    "Sergey A. Melikhov"
  ],
  "comment": "39 pages. An early version of Section 2 was formerly a part of arXiv:1312.2575",
  "categories": [
    "math.LO"
  ],
  "abstract": "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\".",
  "revisions": [
    {
      "version": "v1",
      "updated": "2015-04-13T22:13:29.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "intuitionistic logic",
      "galois connection",
      "tarskis weak elementary geometry",
      "ancient greek tradition",
      "familiar leibniz-euler-venn semantics"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 39,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2015arXiv150403379M"
    }
  }
}