Recognizable Realizability

TL;DR

This paper introduces a new form of realizability based on recognizability with ordinal Turing machines, demonstrating its applicability to Kripke-Platek set theory and its closure properties under intuitionistic provability.

Contribution

It presents a novel notion of realizability based on recognizability rather than computability, expanding the theoretical framework of realizability in set theory.

Findings

All axioms of Kripke-Platek set theory are r-realizable.

The set of r-realizable statements is closed under intuitionistic provability.

Abstract

We introduce a notion of realizability with ordinal Turing machines based on recognizability rather than computability, i.e., the ability to uniquely identify an object. We show that the arising concept of $r$-realizabilty has the property that all axioms of Kripke-Platek set theory are $r$-realizable and that the set of $r$-realizable statements is closed under intuitionistic provability.