__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.