On the number of steps in proofs

DOI10.1016/0168-0072(89)90012-2zbMath0672.03042OpenAlexW2112754349MaRDI QIDQ1119576

Jan Krajíček

Publication date: 1989

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(89)90012-2

zbMATH Keywords

upper bounddepthlengthcut-free proofcut-eliminationcomplexity of proofsnumber of stepsParis-Harrington sentences

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items

The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Some remarks on lengths of propositional proofs, Essential structure of proofs as a measure of complexity, Polynomially and superexponentially shorter proofs in fragments of arithmetic, Generalizing proofs in monadic languages (with a postscript by Georg Kreisel)., Proof lengths for instances of the Paris-Harrington principle, Simulation of Natural Deduction and Gentzen Sequent Calculus, Von Neumann, Gödel and Complexity Theory, A unification-theoretic method for investigating the \(k\)-provability problem, Bounded arithmetic, proof complexity and two papers of Parikh, 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05

Cites Work

• The number of proof lines and the size of proofs in first order logic
• On the length of proofs in formal systems
• A theorem on the formalized arithmetic with function symbols ' and +
• A note on a formalized arithmetic with function symbols ' and +
• Sentences undecidable in formalized arithmetic. An exposition of the theory of Kurt Gödel
• Undecidable theories
• Some applications of formalized consistency proofs
• Some results on speed-up
• Cuts, consistency statements and interpretations
• Speed-Up by Theories with Infinite Models
• Construction of Satisfaction Classes for Nonstandard Models
• One hundred and two problems in mathematical logic
• Bounds for proof-search and speed-up in the predicate calculus
• Abbreviating proofs by adding new axioms
• Existence and feasibility in arithmetic
• Some Results on the Length of Proofs
• Proof theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item