Realisability for Infinitary Intuitionistic Set Theory

DOI10.1016/J.APAL.2023.103259MaRDI QIDQ6349871arXivFDO

Authors Merlin Carl, Lorenzo Galeotti, Robert Paßmann

Publication date 25 September 2020

Published in arXiv

Full work available at URL https://doi.org/10.1016/J.APAL.2023.103259

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Other constructive mathematics (03F65)

arXiv classification

math.LO

Abstract: We introduce a realisability semantics for infinitary intuitionistic set theory that is based on Ordinal Turing Machines (OTMs). 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. Finally, we use a variant of our notion of realisability to show that the propositional admissible rules of (finitary) intuitionistic Kripke-Platek set theory are exactly the admissible rules of intuitionistic propositional logic.

This page was built for publication: Realisability for Infinitary Intuitionistic Set Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6349871)