Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis
Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis
复制标题
经典可实现性中的条形递归：依赖选择和连续统假设
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
J. Krivine
中科院分区：
文献类型：
--
作者：
J. Krivine
本文在经典可实现的背景下研究了棒状递归算子。Berardi、Bezem、Coquand的开创性工作得到了Berger和Oliva的加强。然后，Streicher利用他们的bar递归算子证明了从λ -微积分的常用模型（Scott域、相干空间等）得到的ZF的可实现性模型满足相依选择公理。我们利用经典可实现性的工具对这一结果进行了证明。此外，我们还证明了这些可实现模型满足R的良好有序性和连续介质假设。因此，这些公式是由封闭的lambda_c项实现的。这个新结果允许利用所有这些公理从算术公式的证明中得到程序。
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.