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

From MaRDI portal
Revision as of 10:45, 9 December 2024 by Import241208021249 (talk | contribs) (Normalize DOI.)
scientific article
Language Label Description Also known as
English
The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
scientific article

    Statements

    The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (English)
    0 references
    0 references
    15 January 2010
    0 references
    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)].
    0 references
    survey paper
    0 references
    Kreisel's conjecture
    0 references
    Peano arithmetic
    0 references
    length of proofs
    0 references
    unification
    0 references
    speed-up theorem
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references