On the computational content of the axiom of choice
On the computational content of the axiom of choice
复制标题
论选择公理的计算内容
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
T. Coquand
中科院分区：
文献类型：
--
作者：
S. Berardi;M. Bezem;T. Coquand
摘要利用(可数)选择公理，给出了经典分析负平移的一种可能的计算内容。有趣的是，这种解释使用了荒诞命题的可实现性语义的提炼，这里没有解释为空类型。我们还展示了如何从∃语句的经典分析中的证明计算证据，以及如何从∀∃语句的证明中提取算法。我们的解释在计算上似乎比哥德尔的辩证法解释更直接。
Abstract We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Gödel's Dialectica interpretation.