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

      Realisability for Infinitary Intuitionistic Set Theory

      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

          We introduce a realisability semantics for infinitary intuitionistic set theory that employs Ordinal Turing Machines (OTMs) as realisers. We show that our notion of OTM-realisability is sound with respect to certain systems of infinitary intuitionistic logic, and that all axioms of infinitary Kripke-Platek set theory are realised. As an application of our technique, we show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.

          Related collections

          Author and article information

          Journal
          25 September 2020
          Article
          2009.12172

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

          Custom metadata
          math.LO

          Logic & Foundation

          Comments

          Comment on this article