A MATHEMATICAL COMMITMENT WITHOUT COMPUTATIONAL STRENGTH. Issue 4 (2nd December 2022)

• Record Type: Journal Article
• Authors: FREUND, ANTON
• Is Part Of: Review of symbolic logic. Volume 15:Issue 4(2022)
• Page Start: 880
• Page End: 906
• Publication Date: 2022-12-02
• Subjects: 03F30 -- 03F40 -- 03A05 -- 68R10; independence -- computational strength -- Gödel's second incompleteness theorem -- Hilbert's program -- Kruskal's theorem -- polynomial-time algorithm; Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1017/S1755020321000265
• Languages: English
• ISSNs: 1755-0203

Abstract

Abstract: 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 $\Sigma ^0_2$ -sentences. These sentences assert that each computably enumerable ( $\Sigma ^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 relevant 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 $\Pi ^0_2$ -independence (such as the Paris–Harrington principle), since computational strength provides an extensional invariant on the level of $\Pi ^0_2$ -sentences.