2026-07-20T11:02:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5495 2024-03-06T10:36:13Z ddc:004 open_access

On the Structure of Classical Realizability Models of ZF Krivine, Jean-Louis lambda-calculus Curry-Howard correspondence set theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jean-Louis Krivine 2015 Is Part Of LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2014.146 urn:nbn:de:0030-drops-54953 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.146 eng https://creativecommons.org/licenses/by/3.0/legalcode