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

DOI10.1007/S10958-009-9408-0zbMath1207.03071OpenAlexW1992331170WikidataQ123018765 ScholiaQ123018765MaRDI QIDQ843609

S. Cavagnetto

Publication date: 15 January 2010

Published in: Journal of Mathematical Sciences (New York) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10958-009-9408-0

zbMATH Keywords

survey paperunificationPeano arithmeticspeed-up theoremKreisel's conjecturelength of proofs

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Structure of proofs (03F07) Complexity of proofs (03F20) Gödel numberings and issues of incompleteness (03F40)

Related Items (4)

VARIANTS OF KREISEL’S CONJECTURE ON A NEW NOTION OF PROVABILITY ⋮ Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ On the generation of quantified lemmas ⋮ \(k\)-provability in \(\mathrm{PA}\)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Diophantine induction
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Proof theory. 2nd ed
• The number of proof lines and the size of proofs in first order logic
• A unification algorithm for second-order monadic terms
• On the number of steps in proofs
• The undecidability of the second-order unification problem
• On the length of proofs in formal systems
• Propositional consistency proofs
• A theorem on the formalized arithmetic with function symbols ' and +
• A note on a formalized arithmetic with function symbols ' and +
• Handbook of proof theory
• Note on generalizing theorems in algebraically closed fields
• Bounded arithmetic, proof complexity and two papers of Parikh
• Length and structure of proofs
• A unification-theoretic method for investigating the \(k\)-provability problem
• Generalizing theorems in real closed fields
• Mathematical thought. An introduction to the philosophy of mathematics
• Sentences undecidable in formalized arithmetic. An exposition of the theory of Kurt Gödel
• Some results on speed-up
• Theories very close to PA where Kreisel's Conjecture is false
• Sets of theorems with short proofs
• One hundred and two problems in mathematical logic
• On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
• Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I
• Term Rewriting and All That
• A Machine-Oriented Logic Based on the Resolution Principle
• A Machine-Independent Theory of the Complexity of Recursive Functions
• Abbreviating proofs by adding new axioms
• Existence and feasibility in arithmetic
• Some Results on the Length of Proofs
• Contributions to the Theory of Optimal Control. A General Procedure for the Computation of Switching Manifolds

This page was built for publication: The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem