eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
28:1
28:18
10.4230/LIPIcs.CSL.2024.28
article
Realizability Models for Large Cardinals
Fontanella, Laura
1
https://orcid.org/0000-0003-1588-7524
Geoffroy, Guillaume
2
Matthews, Richard
1
Univ. Paris Est Créteil, LACL, F-94010, France
Université Paris Cité, laboratoire IRIF, France
Realizabilty is a branch of logic that aims at extracting the computational content of mathematical proofs by establishing a correspondence between proofs and programs. Invented by S.C. Kleene in the 1945 to develop a connection between intuitionism and Turing computable functions, realizability has evolved to include not only classical logic but even set theory, thanks to the work of J-L. Krivine. Krivine’s work made possible to build realizability models for Zermelo-Frænkel set theory, ZF, assuming its consistency. Nevertheless, a large part of set theoretic research involves investigating further axioms that are known as large cardinals axioms; in this paper we focus on four large cardinals axioms: the axioms of (strongly) inaccessible cardinal, Mahlo cardinals, measurable cardinals and Reinhardt cardinals. We show how to build realizability models for each of these four axioms assuming their consistency relative to ZFC or ZF.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.28/LIPIcs.CSL.2024.28.pdf
Logic
Classical Realizability
Set Theory
Large Cardinals