Document Open Access Logo

Realizability Models for Large Cardinals

Authors Laura Fontanella , Guillaume Geoffroy, Richard Matthews

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.28.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Author Details

Laura Fontanella
  • Univ. Paris Est Créteil, LACL, F-94010, France
Guillaume Geoffroy
  • Université Paris Cité, laboratoire IRIF, France
Richard Matthews
  • Univ. Paris Est Créteil, LACL, F-94010, France

Funding

  • Matthews, Richard: DIM RFSI 21R03101S.

Acknowledgements

We would like to thank Jean-Louis Krivine for many fruitful discussions that set the main ideas for this work.

Cite AsGet BibTex

Laura Fontanella, Guillaume Geoffroy, and Richard Matthews. Realizability Models for Large Cardinals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.28

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
Keywords
  • Logic
  • Classical Realizability
  • Set Theory
  • Large Cardinals

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  2. Andreas Blass. Exact functors and measurable cardinals. Pacific journal of mathematics, 63(2):335-346, 1976. Google Scholar
  3. Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, and Bruce F. Duba. A syntactic theory of sequential control. Theor. Comput. Sci., 52:205-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90109-5.
  4. Harvey Friedman. The consistency of classical set theory relative to a set theory with intu1tionistic logic. The Journal of Symbolic Logic, 38(2):315-319, 1973. Google Scholar
  5. Harvey Friedman and Andrej Ščedrov. Large sets in intuitionistic set theory. Annals of pure and applied logic, 27(1):1-24, 1984. Google Scholar
  6. Timothy G. Griffin. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47 , 58, 1989. Google Scholar
  7. Joel David Hamkins, Greg Kirmayer, and Norman Lewis Perlmutter. Generalizations of the Kunen inconsistency. Annals of Pure and Applied Logic, 163(12):1872-1890, 2012. Google Scholar
  8. Yair Hayut and Asaf Karagila. Critical cardinals. Israel journal of mathematics, 236(1):449-472, 2020. Google Scholar
  9. Thomas Jech. Set Theory. Springer Monographs in Mathematics. Springer Berlin, Heidelberg, 2003. Google Scholar
  10. Akihiro Kanamori. The higher infinite: large cardinals in set theory from their beginnings. Springer Science & Business Media, 2008. Google Scholar
  11. Stephen Cole Kleene. On the interpretation of intuitionistic number theory. The Journal of Symbolic Logic, 10(4):109-124, 1945. Google Scholar
  12. Jean-Louis Krivine. Typed lambda-calculus in classical Zermelo-Fraenkel set theory. Archive of Mathematical Logic, 40(3):189-205, 2001. Google Scholar
  13. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthéses, Sociètè Mathématique de France, 27:197-229, 2009. Google Scholar
  14. Jean-Louis Krivine. Realizability algebras II: new models of ZF+ DC. Logical Methods in Computer Science, 8:1-28, 2012. Google Scholar
  15. Jean-Louis Krivine. Realizability algebras III: some examples. Mathematical Structures in Computer Science, 28(1):45-76, 2018. Google Scholar
  16. Jean-Louis Krivine. A program for the full axiom of choice. Logical Methods in Computer Science, 17(3):1-22, 2021. Google Scholar
  17. Kenneth Kunen. Elementary embeddings and infinitary combinatorics. The Journal of Symbolic Logic, 36(3):407-413, 1971. Google Scholar
  18. Azriel Lévy. Axiom schemata of strong infinity in axiomatic set theory. Pacific journal of mathematics, 10(1):223-238, 1960. Google Scholar
  19. Richard Matthews. A Guide to Krivine Realizability for Set Theory. arxiv preprint, 2023. URL: https://arxiv.org/abs/2307.13563.
  20. Elliott Mendelson. Introduction to Mathematical Logic. CRC Press, 5 edition, 2009. Google Scholar
  21. Michael Rathjen. Realizing Mahlo set theory in type theory. Archive for Mathematical Logic, 42:89-101, 2003. Google Scholar
  22. Anton Setzer. Extending Martin-Löf type theory by one Mahlo universe. Archive for Mathematical Logic, 39(3):155-181, 2000. Google Scholar
  23. Akira Suzuki. No elementary embedding from V into V is definable from parameters. The Journal of Symbolic Logic, 64(4):1591-1594, 1999. Google Scholar
  24. Neil H. Williams. On Grothendieck universes. Compositio Mathematicae, 21(1):1-3, 1969. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact