Journal article:
Samuel R. Buss.
"The undecidability of k-provability."
Annals of Pure and Applied Logic 53 (1991) 75-102.
Download article: postscript or PDF.
Abstract: The k-provability problem is, given a first order formula~$\phi$ and an integer k, to determine if $\phi$~has a proof consisting of k or fewer lines (i.e., formulas or sequents). This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula~$\phi(x)$ and an integer k such that for all n, $\phi(S^n0)$ has a proof of $\le k$~sequents if and only if $n\in X$.