On the Structure of Classical Realizability Models of ZF

Author Jean-Louis Krivine

Thumbnail PDF


  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Jean-Louis Krivine

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)


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.
  • lambda-calculus
  • Curry-Howard correspondence
  • set theory


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


  1. S. Berardi, M. Bezem, and T. Coquand. On the computational content of the axiom of choice. J. Symb. Logic, 63(2):600-622, 1998. Google Scholar
  2. U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. In Springer, editor, Proc. Logic Colloquium 2001, pages 89-107, 2005. Google Scholar
  3. H.B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958. Google Scholar
  4. T. Griffin. A formulæ-as-type notion of control. In Conf. record 17th A.C.M. Symp. on Principles of Progr. Languages, 1990. Google Scholar
  5. W. Howard. The formulas-as-types notion of construction, pages 479-490. Acad. Press, 1980. Google Scholar
  6. J.-L. Krivine. Realizability algebras : a program to well order ℝ. Logical Methods in Computer Science, 7(3:02):1-47, 2011. Google Scholar
  7. J.-L. Krivine. Realizability algebras II : new models of ZF + DC. Logical Methods in Computer Science, 8(1:10):1-28, 2012. Google Scholar
  8. J.-L. Krivine. Bar recursion in classical realisability : dependent choice and well ordering of ℝ. http://arxiv.org/abs/1502.00112, 2012 (to appear). Google Scholar
  9. J.-L. Krivine. Realizability algebras III : some examples. http://arxiv.org/abs/1210.5065, 2012 (to appear).
  10. T. Streicher. A classical realizability model arising from a stable model of untyped λ-calculus, 2013 (to appear). Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail