The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
type: Item
instance of: scholarly article
title: The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
zbMATH Open document ID: 1207.03071
author: S. Cavagnetto
published in: Journal of Mathematical Sciences (New York)
publication date: 2010-01-15T00:00:00Z
review text: 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 …
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F40
zbMATH DE Number: 5659084
zbMATH Keywords: survey paper
zbMATH Keywords: Kreisel's conjecture
zbMATH Keywords: Peano arithmetic
zbMATH Keywords: length of proofs
zbMATH Keywords: unification
zbMATH Keywords: speed-up theorem
Wikidata QID: Q123018765
MaRDI profile type: Publication
full work available at URL: s10958-009-9408-0
OpenAlex ID: W1992331170
cites work: Unification theory
cites work: Term Rewriting and All That
cites work: Generalizing theorems in real closed fields
cites work: Note on generalizing theorems in algebraically closed fields
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Mathematical thought. An introduction to the philosophy of mathematics
cites work: A Machine-Independent Theory of the Complexity of Recursive Functions
cites work: On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
cites work: Bounded arithmetic, proof complexity and two papers of Parikh
cites work: Handbook of proof theory
cites work: Propositional consistency proofs
cites work: Q5679729
cites work: Abbreviating proofs by adding new axioms
cites work: Q3697944
cites work: A unification algorithm for second-order monadic terms
cites work: A unification-theoretic method for investigating the \(k\)-provability problem
cites work: One hundred and two problems in mathematical logic
cites work: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
cites work: The undecidability of the second-order unification problem
cites work: Theories very close to PA where Kreisel's Conjecture is false
cites work: Diophantine induction
cites work: Q5812175
cites work: On the number of steps in proofs
cites work: Q3786479
cites work: The number of proof lines and the size of proofs in first order logic
cites work: Q4146913
cites work: Q5613949
cites work: Contributions to the Theory of Optimal Control. A General Procedure for the Computation of Switching Manifolds
cites work: On the length of proofs in formal systems
cites work: Sentences undecidable in formalized arithmetic. An exposition of the theory of Kurt Gödel
cites work: Q3816071
cites work: Q5187274
cites work: Some Results on the Length of Proofs
cites work: Length and structure of proofs
cites work: Existence and feasibility in arithmetic
cites work: Q3893931
cites work: Q4215637
cites work: Q3815293
cites work: Sets of theorems with short proofs
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Handbook of automated reasoning. In 2 vols
cites work: Proof theory. 2nd ed
cites work: A theorem on the formalized arithmetic with function symbols ' and +
cites work: A note on a formalized arithmetic with function symbols ' and +
cites work: Some results on speed-up
DOI: 10.1007/S10958-009-9408-0
description: scientific article; zbMATH DE number 5659084