Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

Krivine, Jean-Louis

doi:10.4230/LIPIcs.CSL.2016.25

File

LIPIcs.CSL.2016.25.pdf

Filesize: 496 kB
11 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2016.25
URN: urn:nbn:de:0030-drops-65650

Author Details

Jean-Louis Krivine

Cite AsGet BibTex

Jean-Louis Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 25:1-25:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.25

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.

Keywords

lambda-calculus
Curry-Howard correspondence
set theory

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.
E. Engeler. Algebras and combinators. Algebra Universalis, 13(1):389-392, 1981.
T. Griffin. A formulae-as-type notion of control. In Proc. of the 17th ACM. Symp. on Principles of Progr. Languages, pages 47-58, 1990. URL: http://dx.doi.org/10.1145/96709.96714.
W. Howard. The formulas-as-types notion of construction. In Essays on combinatory logic, λ-calculus, and formalism, 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. Realizability algebras III: some examples, 2012 (to appear in Math. Struct. Comp. Sc.). URL: http://arxiv.org/abs/1210.5065.
J.-L. Krivine. On the structure of classical realizability models of ZF, 2014 (to appear in Proceedings Types 2014). URL: http://arxiv.org/abs/1408.1868.
C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In Recursive function theory: Proc. Symp. in pure math. vol. 5, Amer. Math. Soc. Providence, Rhode Island, pages 1-27, 1962.
T. Streicher. A classical realizability model arising from a stable model of untyped λ-calculus, 2013 (to appear).