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.CSL.2016.25
URN: urn:nbn:de:0030-drops-65650
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6565/
Go to the corresponding LIPIcs Volume Portal

Krivine, Jean-Louis

Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

pdf-format:
LIPIcs-CSL-2016-25.pdf (0.5 MB)

Abstract

This paper is about the bar recursion operator in the context of classical realizability. The pioneering work of Berardi, Bezem, Coquand was enhanced by Berger and Oliva. Then Streicher has shown, by means of their bar recursion operator, that the realizability models of ZF, obtained from usual models of lambda-calculus (Scott domains, coherent spaces, ...), satisfy the axiom of dependent choice. We give a proof of this result, using the tools of classical realizability. Moreover, we show that these realizability models satisfy the well ordering of R and the continuum hypothesis. These formulas are therefore realized by closed lambda_c-terms. This new result allows to obtain programs from proofs of arithmetical formulas using all these axioms.

BibTeX - Entry

@InProceedings{krivine:LIPIcs:2016:6565,
  author =	{Jean-Louis Krivine},
  title =	{{Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{25:1--25:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Jean-Marc Talbot and Laurent Regnier},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6565},
  URN =		{urn:nbn:de:0030-drops-65650},
  doi =		{10.4230/LIPIcs.CSL.2016.25},
  annote =	{Keywords: lambda-calculus, Curry-Howard correspondence, set theory}
}

Keywords: lambda-calculus, Curry-Howard correspondence, set theory
Collection: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
Issue Date: 2016
Date of publication: 29.08.2016

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