论文标题
没有计算强度的数学承诺
A mathematical commitment without computational strength
论文作者
论文摘要
我们提出了戈德尔第二次不完整定理的新表现，并讨论了其基本意义，尤其是在希尔伯特计划方面。具体来说，我们考虑了Peano Arithmetic（$ \ Mathbf {pa} $）的适当扩展，该扩展由数学上有意义的公理方案，该方案由$σ^0_2 $ -Sentences组成。这些句子断言，有限二进制树的每个计算枚举（$σ^0_1 $ - 可定义）属性都有有限的基础。由于这一事实需要多项式时间算法的存在，因此对计算机科学很重要。从技术层面上讲，我们的公理方案是由于哈维·弗里德曼（Harvey Friedman）引起的独立结果的变体。同时，我们的公理方案的元数学特性将其与大多数已知的独立性结果区分开：由于其逻辑复杂性，我们的公理方案不会增加计算强度。建立独立性的唯一已知方法取决于戈德尔的第二个不完整定理。相反，对于$π^0_2 $独立性的典型示例（例如巴黎 - 哈灵顿原理）的典型示例不需要Gödel定理，因为计算强度在$π^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.
