On Gödel’s Theorems on Lengths of Proofs II: Lower Bounds for Recognizing k Symbol Provability
Samuel R. Buss · Birkhäuser Boston eBooks · 1995
This paper discusses a claim made by Gödel in a letter to von Neumann which is closely related to the P versus NP problem. Gödel’s claim is that k -symbol provability in first-order logic can not be decided in o ( k ) time on a deterministic Turing machine. We prove Gödel’s claim and also prove a conjecture of S. Cook’s that this problem can not be decided in o ( k / log k ) time by a nondeterministic Turing machine. In addition, we prove that the k -symbol provability problem is NP -complete, even for provability in propositional logic.