Bar recursion in classical realisability: dependent choice and continuum hypothesis

DOI10.4230/LIPICS.CSL.2016.25MaRDI QIDQ5278411zbMATH OpenFDO

Authors Jean-Louis Krivine

Publication date 19 July 2017

Full work available at URL https://arxiv.org/abs/1502.00112

zbMATH Keywords

\(\lambda\)-calculusCurry-Howard correspondenceset theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Axiom of choice and related propositions (03E25) Consistency and independence results (03E35) Continuum hypothesis and Martin's axiom (03E50)

Abstract: This paper is about the bar recursion operator in the context of classical realizability. After the pioneering work of Berardi, Bezem & Coquand [1], T. Streicher has shown [10], 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 $mathbbR$ and the continuum hypothesis These formulas are therefore realized by closed $lambd{a}_c$-terms. This allows to obtain programs from proofs of arithmetical formulas using all these axioms.

Recommendations

• On bar recursion and choice in a classical setting
• scientific article; zbMATH DE number 2222013
• Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice
• On the computational content of the axiom of choice
• Dependent choice, `quote' and the clock

Cited in

(10)

• Contingent objects and the Barcan formula
• On bar recursion and choice in a classical setting
• A classical realizability model arising from a stable model of untyped lambda calculus
• Programming and Proving with Classical Types
• A program for the full axiom of choice
• Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice
• scientific article; zbMATH DE number 2222013 (Why is no real title available?)
• Stateful Realizers for Nonstandard Analysis
• A direct computational interpretation of second-order arithmetic via update recursion
• Realizability with stateful computations for nonstandard analysis

This page was built for publication: Bar recursion in classical realisability: dependent choice and continuum hypothesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5278411)