arXiv · 2009.12172
Realisability for Infinitary Intuitionistic Set Theory
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.
Explore related subjects
Keep this discovery
Merlin Carl, Lorenzo Galeotti, Robert Passmann. 2020-09-25. Realisability for Infinitary Intuitionistic Set Theory. https://arxiv.org/abs/2009.12172
Cite the original work for its findings. Save a collection to share your selection of sources.