Document Open Access Logo

Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis

Author Jean-Louis Krivine

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2016.25.pdf
  • Filesize: 496 kB
  • 11 pages

Document Identifiers

Subject Classification

Keywords
  • lambda-calculus
  • Curry-Howard correspondence
  • set theory

Metrics

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

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.

Cite As Get 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

Author Details

Jean-Louis Krivine

References

  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. E. Engeler. Algebras and combinators. Algebra Universalis, 13(1):389-392, 1981. Google Scholar
  5. 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.
  6. W. Howard. The formulas-as-types notion of construction. In Essays on combinatory logic, λ-calculus, and formalism, pages 479-490. Acad. Press, 1980. Google Scholar
  7. J.-L. Krivine. Realizability algebras: a program to well order ℝ. Logical Methods in Computer Science, 7(3:02):1-47, 2011. Google Scholar
  8. J.-L. Krivine. Realizability algebras II: new models of ZF + DC. Logical Methods in Computer Science, 8(1:10):1-28, 2012. Google Scholar
  9. J.-L. Krivine. Realizability algebras III: some examples, 2012 (to appear in Math. Struct. Comp. Sc.). URL: http://arxiv.org/abs/1210.5065.
  10. 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.
  11. 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. Google Scholar
  12. T. Streicher. A classical realizability model arising from a stable model of untyped λ-calculus, 2013 (to appear). Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact