The undecidability of \(k\)-provability (Q1176199)

The \(k\)-provability problem is to decide of any (first order) formula \(\varphi\) and natural number \(k\) whether \(\varphi\) can be proved within \(k\) lines. The autor gives a negative answer for sequent calculi. More precisely, the ``Main Theorem'' states: Let LK be Gentzen's sequent calculus with a unary function symbol \(S\), a binary function symbol and infinitely many binary relation symbols. Then for each r.e. set \(X\) one can find a formula \(\varphi(x)\) and a natural number \(k\) such that \(n\in X\) iff the sequent \(\to\varphi(S^ n0)\) has a proof with \(\leq k\) distinct sequents, for all \(n\). A similar result is shown for the calculus with equality, in which equality axioms are confined to atomic formulas. Details are quoted, because the result is sensitive to the formulation of formal systems. Indeed, there are positive results of Farmer where, in \(\forall x\varphi(x)\supset\varphi(t)\), some conditions are imposed on \(t\), and of Krajiček and Pudlák where the cut rule is excluded. And the author gives a caution: ``Unfortunately, our proof does not seem to apply immediately to all usual first order logics''. His proof roughly goes as follows. First, a second order unification problem is shown to be undecidable, by translating Diophantine equations into the unification format. Then, for each unification problem, the author produces a formula \(\varphi\) and a number \(k\) (second order free variables in the unification problem are turned into first order bound variables) such that the problem has a solution iff \(\to\varphi\) has a proof of \(\leq k\) lines. (The formula \(\varphi\) is provable in a straightforward manner; but a solution to the unification problem gives a shorter proof.) Of course, to show this equivalence, a detailed analysis of formal proofs is required, which the author does by employing such notions as logic flow graphs. The work in this paper is, like others, motivated by the so-called Kreisel conjecture: If \(\text{PA}\vdash\varphi(S^ n 0)\) for all \(n\) within a common bound, then: \(\text{PA}\vdash\forall x\varphi(x)\)?