Research article:

    Samuel R. Buss.
    "On Gödel's theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability"
    In Feasible Mathematics II, P. Clote and J. Remmel (eds),
    Birkhauser, 1995, pp. 57-90.

    Download article: postscript or PDF

    From the introduction: 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.

    The paper also include Peter Clote's translation of a letter from Gödel to von Neumann discussing issues related to the P versus NP problem.

Back to Sam Buss's publications page.