2020/09/25 by Carl, Merlin, Galeotti, Lorenzo, Passmann, Robert
#FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.2009.12172
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.