License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.146
URN: urn:nbn:de:0030-drops-54953
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5495/
Go to the corresponding LIPIcs Volume Portal

Krivine, Jean-Louis

On the Structure of Classical Realizability Models of ZF

pdf-format:
9.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{krivine:LIPIcs:2015:5495,
  author =	{Jean-Louis Krivine},
  title =	{{On the Structure of Classical Realizability Models of ZF}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{146--161},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5495},
  URN =		{urn:nbn:de:0030-drops-54953},
  doi =		{10.4230/LIPIcs.TYPES.2014.146},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}

Keywords: lambda-calculus, Curry-Howard correspondence, set theory
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI