Hybrid realizability for intuitionistic and classical choice
Hybrid realizability for intuitionistic and classical choice
复制标题
直觉和经典选择的混合可实现性
DOI：
10.1145/2933575.2934511
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Blot V
中科院分区：
文献类型：
--
作者：
Blot V
在像Kleene或Kreisel的直觉可实现性中，选择公理是平凡地实现的。它甚至可以在马丁-洛夫的直觉类型理论中证明。然而，在经典逻辑中，即使是较弱的可数选择公理也证明了不可计算函数的存在。这种逻辑上的优势是以复杂的计算解释为代价的，其中涉及到像bar递归这样的强递归方案。我们从两个世界中取最好的，并定义了一个可实现的算术模型和公理的选择，其中包括直觉和经典推理。在这个模型中，选择公理的两个版本可以共存于一个证明中：直觉选择和经典可数选择。我们有效地解释了直觉选择，但它的前提不能来自经典推理。相反，我们的经典选择版本在完全经典逻辑中是有效的，但它仅限于可数的情况，其实现者涉及酒吧递归。拥有这两个版本使我们能够获得有效的提取程序，同时保持经典逻辑的可证明性强度。
In intuitionistic realizability like Kleene's or Kreisel's, the axiom of choice is trivially realized. It is even provable in Martin-Löf's intuitionistic type theory. In classical logic, however, even the weaker axiom of countable choice proves the existence of non-computable functions. This logical strength comes at the price of a complicated computational interpretation which involves strong recursion schemes like bar recursion. We take the best from both worlds and define a realizability model for arithmetic and the axiom of choice which encompasses both intuitionistic and classical reasoning. In this model two versions of the axiom of choice can co-exist in a single proof: intuitionistic choice and classical countable choice. We interpret intuitionistic choice efficiently, however its premise cannot come from classical reasoning. Conversely, our version of classical choice is valid in full classical logic, but it is restricted to the countable case and its realizer involves bar recursion. Having both versions allows us to obtain efficient extracted programs while keeping the provability strength of classical logic.
登录
查看更多内容
DOI：
--
发表时间：
1994
期刊：
Journal of Symbolic Logic (JSL)
影响因子：
--
作者：
S. Berardi;M. Bezem;T. Coquand
通讯作者：
T. Coquand
经典逻辑的可实现性
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
J. Krivine
通讯作者：
J. Krivine
改进的条形递归和经典相关选择
DOI：
--
发表时间：
2004
期刊：
影响因子：
--
作者：
Ulrich Berger;Paulo Oliva
通讯作者：
Paulo Oliva
DOI：
10.1017/cbo9780511983504.002
发表时间：
1998-08
期刊：
Acta Mathematica Sinica, English Series
影响因子：
--
作者：
R. Amadio;P. Curien
通讯作者：
R. Amadio;P. Curien
λ μ 微积分的延拓模型的完备性
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
M. Hofmann
通讯作者：
M. Hofmann