辩证逻辑原理
Dialectica Logical Principles
摘要：
哥德尔的Dialectica解释旨在获得海廷算术的相对兼容性证明，与双重否定解释一起使用，以获得皮亚诺算术的相容性。近年来，基于哥德尔辩证法解释的证明理论转换（所谓的证明解释）已被系统地用于从证明中提取新内容，因此解释在数学和计算机科学的几个领域中找到了相关的应用。继我们以前的工作哥德尔纤维化，我们提出了一个（超）学说的辩证法，这完全符合解释的逻辑描述的特点。说明我们在范畴论中导出了对蕴涵联结词的解释的可靠性，正如斯佩克特和特罗尔斯特拉所阐明的那样。这就要求有超越直觉主义逻辑、马尔可夫原理（MP）和先验独立性（IP）原则的额外逻辑原则，以及一定的选择。我们展示了这些原则是如何满足的范畴设置，建立一个紧密的（内部语言）之间的对应关系的逻辑系统和范畴框架。这种紧密的对应关系不仅在讨论已经知道的辩证法的应用时应该很方便，比如它用于从（一些）经典定理中提取计算内容（证明挖掘），它用于帮助建模特定的抽象机器等，而且还有助于设计新的应用。
英文摘要：
Gödel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are based on Gödel's Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on Gödel fibrations, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markov's Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
