A Note on OTM-Realizability and Constructive Set Theories
Logic
2024-03-18 v2
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.
Keywords
Cite
@article{arxiv.1903.08945,
title = {A Note on OTM-Realizability and Constructive Set Theories},
author = {Merlin Carl},
journal= {arXiv preprint arXiv:1903.08945},
year = {2024}
}