• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Hybrid realizability for intuitionistic and classical choice
【24h】

Hybrid realizability for intuitionistic and classical choice

机译：直觉和经典选择的混合实现

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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.
机译：在像克莱因（Kleene）或克雷塞尔（Kreisel）这样的直觉可实现性中，选择公理被轻易实现了。马丁·洛夫的直觉类型理论甚至可以证明这一点。但是，在经典逻辑中，即使是可数选择的较弱公理也证明了不可计算的函数的存在。这种逻辑上的优势是以复杂的计算解释为代价的，其中涉及强大的递归方案（如bar递归）。我们从两个方面都吸取了最大的优势，并为算术和选择公理定义了一个可实现性模型，其中包括直觉推理和经典推理。在这个模型中，选择公理的两个版本可以在一个证明中共存：直觉选择和经典可数选择。我们有效地解释了直觉选择，但是它的前提不能来自经典推理。相反，我们的经典选择版本在完全经典逻辑中有效，但仅限于可数情况，其实现者涉及小​​节递归。拥有两个版本都可以使我们获得有效的提取程序，同时保持经典逻辑的可证明性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号