LIPIcs.TYPES.2014.146.pdf
- Filesize: 0.53 MB
- 16 pages
Document
On the Structure of Classical Realizability Models of ZF
Author
-
Part of:
Volume:
20th International Conference on Types for Proofs and Programs (TYPES 2014)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-10-12
Cite AsGet BibTex
Jean-Louis Krivine. On the Structure of Classical Realizability Models of ZF. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 146-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TYPES.2014.146
https://doi.org/10.4230/LIPIcs.TYPES.2014.146
Abstract
The technique of classical realizability is an extension of the method of forcing; it permits to extend the Curry-Howard correspondence between proofs and programs, to Zermelo-Fraenkel set theory and to build new models of ZF, called realizability models. The structure of these models is, in general, much more complicated than that of the particular case of forcing models.
We show here that the class of constructible sets of any realizability model is an elementary extension of the constructibles of the ground model (a trivial fact in the case of forcing, since these classes are identical).
By Shoenfield absoluteness theorem, it follows that every true Sigma^1_3 formula is realized by a closed lambda_c-term.
Keywords
- lambda-calculus
- Curry-Howard correspondence
- set theory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
S. Berardi, M. Bezem, and T. Coquand. On the computational content of the axiom of choice. J. Symb. Logic, 63(2):600-622, 1998.
-
U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. In Springer, editor, Proc. Logic Colloquium 2001, pages 89-107, 2005.
-
H.B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958.
-
T. Griffin. A formulæ-as-type notion of control. In Conf. record 17th A.C.M. Symp. on Principles of Progr. Languages, 1990.
-
W. Howard. The formulas-as-types notion of construction, pages 479-490. Acad. Press, 1980.
-
J.-L. Krivine. Realizability algebras : a program to well order ℝ. Logical Methods in Computer Science, 7(3:02):1-47, 2011.
-
J.-L. Krivine. Realizability algebras II : new models of ZF + DC. Logical Methods in Computer Science, 8(1:10):1-28, 2012.
-
J.-L. Krivine. Bar recursion in classical realisability : dependent choice and well ordering of ℝ. http://arxiv.org/abs/1502.00112, 2012 (to appear).
- J.-L. Krivine. Realizability algebras III : some examples. http://arxiv.org/abs/1210.5065, 2012 (to appear).
-
T. Streicher. A classical realizability model arising from a stable model of untyped λ-calculus, 2013 (to appear).