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

Back to Sam Buss's publications page.