__Journal article:__

** Samuel R. Buss.
"The undecidability of k-provability."
**

** 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$.