Realisability for Infinitary Intuitionistic Set Theory

TL;DR

This paper develops a new realisability semantics for infinitary intuitionistic set theory using Ordinal Turing Machines, establishing soundness and characterizing admissible rules within this framework.

Contribution

It introduces an OTM-based realisability semantics for infinitary intuitionistic set theory and connects it to logical admissibility properties.

Findings

OTM-realisability is sound for certain infinitary intuitionistic systems

All axioms of infinitary Kripke-Platek set theory are realised

Admissible propositional rules match those of intuitionistic propositional logic

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.