18
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Mathematical semantics of intuitionistic logic

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          This work is a mathematician's attempt to understand intuitionistic logic. It can be read in two ways: as a research paper interspersed with lengthy digressions into rethinking of standard material; or as an elementary (but highly unconventional) introduction to first-order intuitionistic logic. For the latter purpose, no training in formal logic is required, but a modest literacy in mathematics, such as topological spaces and posets, is assumed. The main theme of this work is the search for a formal semantics adequate to Kolmogorov's informal interpretation of intuitionistic logic (whose simplest part is more or less the same as the so-called BHK interpretation). This search goes beyond the usual model theory, based on Tarski's notion of semantic consequence, and beyond the usual formalism of first-order logic, based on schemata. Thus we study formal semantics of a simplified version of Paulson's meta-logic, used in the Isabelle prover. By interpreting the meta-logical connectives and quantifiers constructively, we get a generalized model theory, which covers, in particular, realizability-type interpretations of intuitionistic logic. On the other hand, by analyzing Kolmogorov's notion of semantic consequence (which is an alternative to Tarski's standard notion), we get an alternative model theory. By using an extension of the meta-logic, we further get a generalized alternative model theory, which suffices to formalize Kolmogorov's semantics. On the other hand, we also formulate a modification of Kolmogorov's interpretation, which is compatible with the usual, Tarski-style model theory. Namely, it can be formalized by means of sheaf-valued models, which turn out to be a special case of Palmgren's categorical models; intuitionistic logic is complete with respect to this semantics.

          Related collections

          Most cited references53

          • Record: found
          • Abstract: not found
          • Article: not found

          topological spaces

            Bookmark
            • Record: found
            • Abstract: found
            • Article: found
            Is Open Access

            Homotopy theoretic models of identity types

            This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              The Incompleteness Theorems

                Bookmark

                Author and article information

                Journal
                2015-04-13
                2017-05-01
                Article
                1504.03380
                bbe2433d-7e3f-4c56-ae36-8fc5179ef7ee

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                179 pages. Most results mentioned in the abstract are new. Much of the previous version (which was 77 pages) is completely rewritten
                math.LO

                Logic & Foundation
                Logic & Foundation

                Comments

                Comment on this article