The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (Q843609): Difference between revisions

The paper is for the most part a survey of known results related to Kreisel's conjecture (KC). The original problem, posed by Kreisel in the early 70s, asks whether the following holds: For every arithmetical formula \(\phi(x)\), if there is a \(k\) such that for all \(n\), \(\phi(S^n(0))\) is provable in the usual axiomatic system for Peano arithmetic (PA) in at most \(k\) steps, then PA proves \(\forall x\,\phi(x)\). The paper mentions various partial or related results, such as \textit{R. J. Parikh}'s proof of KC for a variant of PA where \(+\) and \(\times\) are replaced by ternary predicates [Trans. Am. Math. Soc. 177, 29--36 (1973; Zbl 0269.02011)], results of \textit{T. Yukami} [Tsukuba J. Math. 1, 195--211 (1977; Zbl 0392.03036); Tsukuba J. Math. 2, 69--73 (1978; Zbl 0411.03052)] and \textit{V. P. Orevkov} [Semiotika i Inf. 12, 37--38 (1979; Zbl 0665.03040)] on similar modifications of PA, the proof of KC for finite fragments of arithmetic by \textit{T. Miyatake} [Tsukuba J. Math. 4, 115--125 (1980; Zbl 0493.03034)], and results of \textit{P. Hrubeš} [J. Symb. Log. 72, No.~1, 123--137 (2007; Zbl 1117.03065)] on slightly enriched versions of PA for which KC fails. In \S 4, the paper discusses in detail approaches to KC based on unification (proposed explicitly by Baaz, but already implicit in Parikh's work). Particular attention is given to results of \textit{J. Krajíček} and \textit{P. Pudlák} [Arch. Math. Logic 27, No.~1, 69--84 (1988; Zbl 0644.03032)], \textit{W. M. Farmer} [Ann. Pure Appl. Logic 51, No.~3, 173--214 (1991; Zbl 0735.03001)], and \textit{M. Baaz} and \textit{P. Pudlák} [in: P. Clote et al. (eds.), Arithmetic, proof theory, and computational complexity. Oxford: Clarendon Press. Oxf. Logic Guides. 23, 30--60 (1993; Zbl 0812.03024)]. Then the paper turns to a somewhat different subject, namely the following claim by \textit{K. Gödel} [Erg. Math. Kolloqu. 7, 23--24 (1936; Zbl 0014.24102)]: If \(Z\) is a formal system of \(i\)th-order arithmetic and \(T\) is \((i+1)\)th-order arithmetic, then for any recursive function \(f\) there is a formula provable in \(Z\) with a \(T\)-proof of length \(k\) whose shortest \(Z\)-proof has length at least \(f(k)\). The paper discusses generalizations of Gödel's statement proved by Parikh [loc. cit.], \textit{J. Krajíček} [Ann. Pure Appl. Logic 41, No.~2, 153--178 (1989; Zbl 0672.03042)], and \textit{S. R. Buss} [J. Symb. Log. 59, No.~3, 737--756 (1994; Zbl 0805.03047)], as well as related results by \textit{A. Ehrenfeucht} and \textit{J. Mycielski} [Bull. Am. Math. Soc. 77, 366--367 (1971; Zbl 0216.01002)] and \textit{R. Parikh} [J. Symb. Log. 36, 494--508 (1971; Zbl 0243.02037)]. Finally, the author considers connections between Gödel's speed-up theorem and Kreisel's conjecture, including his own results presented at Logic Colloquium 2005 [in: S. S. Wainer (ed.), Bull. Symb. Log. 12, No.~2, 327--328 (2006; Zbl 1107.03303)].