2019/03/21 by Merlin Carl, Carl, Merlin
Computer Science · Psychology · #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Philosophy and Theoretical Science
paper · pdf · doi:10.48550/arxiv.1903.08945
openalex publication_date 2019/03/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.