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.