Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).

DOI10.1016/J.APAL.2007.10.010zbMATH Open1153.03040OpenAlexW2030319866MaRDI QIDQ930260FDOQ930260

Authors Matthias Baaz, Piotr Wojtylak 

Publication date 23 June 2008

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

Full work available at URL https://doi.org/10.1016/j.apal.2007.10.010

zbMATH Keywords

proof complexitygeneralization of proofsmodification of Kreisel's conjecturemonadic languagepartial proof datauniform derivability of a proof schema

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07) First-order arithmetic and fragments (03F30)

Recommendations

• scientific article; zbMATH DE number 4087658
• Theories very close to PA where Kreisel's Conjecture is false
• Kreisel's Conjecture with minimality principle
• The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
• scientific article; zbMATH DE number 4072964
• The undecidability of \(k\)-provability
• scientific article; zbMATH DE number 3959390
• Bounded Induction and Satisfaction Classes
• Simple axioms that are obviously true in \(\mathbb{N}\)
• The Kreisel length-of-proof problem

Cites work

• scientific article; zbMATH DE number 440473 (Why is no real title available?)
• scientific article; zbMATH DE number 440474 (Why is no real title available?)
• scientific article; zbMATH DE number 3167494 (Why is no real title available?)
• scientific article; zbMATH DE number 3841940 (Why is no real title available?)
• scientific article; zbMATH DE number 3933037 (Why is no real title available?)
• scientific article; zbMATH DE number 4039891 (Why is no real title available?)
• scientific article; zbMATH DE number 3577484 (Why is no real title available?)
• scientific article; zbMATH DE number 481931 (Why is no real title available?)
• scientific article; zbMATH DE number 515726 (Why is no real title available?)
• scientific article; zbMATH DE number 976360 (Why is no real title available?)
• scientific article; zbMATH DE number 1555175 (Why is no real title available?)
• A theorem on generalizations of proofs
• A unification algorithm for second-order monadic terms
• Arithmetic on curves
• Foundations of mathematics for the working mathematician
• Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
• On the number of steps in proofs
• One hundred and two problems in mathematical logic
• Proof theory
• Recursive Functions of One Variable
• Sets of theorems with short proofs
• Some Results on the Length of Proofs
• Some applications of formalized consistency proofs
• The number of proof lines and the size of proofs in first order logic
• The undecidability of \(k\)-provability
• The undecidability of the second-order unification problem

Cited in

(15)

• scientific article; zbMATH DE number 4087658 (Why is no real title available?)
• scientific article; zbMATH DE number 4135936 (Why is no real title available?)
• A theorem on generalizations of proofs
• Taking out LK parts from a proof in Peano arithmetic
• scientific article; zbMATH DE number 3321243 (Why is no real title available?)
• A Proof-theoretic Treatment of Assignments
• Note on the benefit of proof representations by name
• On the proof-theoretic foundation of general definition theory
• Herbrand's theorem and term induction
• scientific article; zbMATH DE number 4033743 (Why is no real title available?)
• scientific article; zbMATH DE number 1948175 (Why is no real title available?)
• scientific article; zbMATH DE number 4072964 (Why is no real title available?)
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
• scientific article; zbMATH DE number 2006629 (Why is no real title available?)
• scientific article; zbMATH DE number 4152372 (Why is no real title available?)

This page was built for publication: Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q930260)