Realisability for Infinitary Intuitionistic Set Theory
Logic
2022-12-14 v3
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.
Keywords
Cite
@article{arxiv.2009.12172,
title = {Realisability for Infinitary Intuitionistic Set Theory},
author = {Merlin Carl and Lorenzo Galeotti and Robert Passmann},
journal= {arXiv preprint arXiv:2009.12172},
year = {2022}
}