arXiv · 1903.08945
A Note on OTM-Realizability and Constructive Set Theories
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.
Explore related subjects
Keep this discovery
Merlin Carl. 2019-03-21. A Note on OTM-Realizability and Constructive Set Theories. https://arxiv.org/abs/1903.08945
Cite the original work for its findings. Save a collection to share your selection of sources.