没有计算能力的数学承诺
A mathematical commitment without computational strength
摘要：
我们提出了哥德尔第二不完备性定理的一种新的表现形式，并讨论了它的基础意义，特别是关于希尔伯特的计划。具体地说，我们认为适当的扩展皮亚诺算术（$\mathbf{PA}$）的数学上有意义的公理计划，由$Σ^0_2$ -句子。这些句子断言，有限二叉树的每个可计算的（$Σ^0_1$ -可定义的，没有参数）属性都有一个有限基。由于这一事实需要存在多项式时间算法，它是重要的计算机科学。在技术层面上，我们的公理方案是哈维·弗里德曼（Harvey Friedman）的独立性结果的变体。与此同时，我们的公理方案的元数学性质将其与大多数已知的独立性结果区分开来：由于其逻辑复杂性，我们的公理方案不会增加计算强度。唯一已知的方法来建立其独立性依赖于哥德尔的第二不完全性定理。相比之下，对于$Π^0_2$ -独立性的典型示例（例如巴黎-哈灵顿原理），不需要哥德尔定理，因为计算强度提供了$Π^0_2$ -句子水平上的扩展不变量。
英文摘要：
We present a new manifestation of Gödel's second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert's program. Specifically, we consider a proper extension of Peano arithmetic ($\mathbf{PA}$) by a mathematically meaningful axiom scheme that consists of $Σ^0_2$-sentences. These sentences assert that each computably enumerable ($Σ^0_1$-definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is important for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel's second incompleteness theorem. In contrast, Gödel's theorem is not needed for typical examples of $Π^0_2$-independence (such as the Paris-Harrington principle), since computational strength provides an extensional invariant on the level of $Π^0_2$-sentences.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
