A Note on OTM-Realizability and Constructive Set Theories

TL;DR

This paper introduces an ordinalized realizability interpretation using ordinal Turing machines, applying it to set theory axioms, and explores which axioms of IZF and CZF are realizable.

Contribution

It extends Kleene's realizability to set theory using OTMs, providing a new perspective on the realizability of set-theoretic axioms.

Findings

All axioms of intuitionistic first-order logic are OTM-realizable.

The paper discusses which axioms of IZF and CZF are OTM-realizable.

Preliminary sketches suggest broad realizability results.

Abstract

We define an ordinalized version of Kleene's realizability interpretation of intuitionistic logic by replacing Turing machines with Koepke's ordinal Turing machines (OTMs), thus obtaining a notion of realizability applying to arbitrary statements in the language of set theory. We observe that every instance of the axioms of intuitionistic first-order logic are OTM-realizable and consider the question which axioms of Friedman's Intuitionistic Set Theory (IZF) and Aczel's Constructive Set Theory (CZF) are OTM-realizable. This is an introductory note, and proofs are mostly only sketched or omitted altogether. It will soon be replaced by a more elaborate version.