zbMATH — the first resource for mathematics

The undecidability of \(k\)-provability. (English) Zbl 0749.03039
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)\)?

03F20 Complexity of proofs
03B25 Decidability of theories and sets of sentences
Full Text: DOI
[1] Farmer, W.M., A unification-theoretic method for investigating the k-provability problem, Ann. pure appl. logic, 51, 173-214, (1991) · Zbl 0735.03001
[2] Farmer, W.M., A unification algorithm for second-order monadic terms, Ann. pure appl. logic, 39, 131-174, (1988) · Zbl 0655.03004
[3] Girard, J.Y., Linear logic, Theoret. comput. sci., 50, 1-102, (1987) · Zbl 0625.03037
[4] Goldfarb, W.D., The undecidability of the second-order unification problem, Theoret. comput. sci., 13, 225-230, (1981) · Zbl 0457.03006
[5] Krajíček, J., (), 82-99, Proc. Fifth Easter Conf. on Model Theory, Seminarberichte 93
[6] Krajíček, J.; Pudlák, P., The number of proof lines and the size of proofs in first-order logic, Arch. math. logic, 27, 69-84, (1988) · Zbl 0644.03032
[7] G. Kreisel, Proof theory: some personal recollections, Appendix to [13]
[8] Miyatake, T., On the length of proofs in a formal system of recursive arithmetic, logic symposia, hakone, (), 81-108
[9] Miyatake, T., On the length of proofs in formal systems, Tsukuba J. math., 4, 115-125, (1980) · Zbl 0493.03034
[10] Orevkov, V.P., Reconstruction of a proof form its scheme, Soviet math. dokl., Original Russian version in dokl. akad. nauk., 293, 313-316, (1987) · Zbl 0638.03053
[11] Parijh, R.J., Some results on the lengths of proofs, Trans. amer. math. soc., 177, 29-36, (1973)
[12] Richardson, D., Sets of theorems with short proofs, J. symbolic logic, 39, 235-242, (1974) · Zbl 0291.02021
[13] Takeuti, G., Proof theory, (1987), North-Holland Amsterdam
[14] Yukami, T., A theorem on the formalized arithmetic with function symbols ’ and +, Tsukuba J. math., 1, 195-211, (1977) · Zbl 0392.03036
[15] Yukami, T., A note on a formalized arithmetic with function symbols ’ and +, Tsukuba J. math., 2, 69-73, (1978) · Zbl 0411.03052
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.