Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis
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.
lambda-calculus
Curry-Howard correspondence
set theory
25:1-25:11
Regular Paper
Jean-Louis
Krivine
Jean-Louis Krivine
10.4230/LIPIcs.CSL.2016.25
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.
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.
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.
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).
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode