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

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

Piotr Wojtylak, Matthias Baaz

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

Recommendations

• scientific article
• 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
• 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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• One hundred and two problems in mathematical logic
• Proof theory
• Title not available (Why is that?)
• The number of proof lines and the size of proofs in first order logic
• Some Results on the Length of Proofs
• Foundations of mathematics for the working mathematician
• Title not available (Why is that?)
• Title not available (Why is that?)
• On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics
• On the number of steps in proofs
• The undecidability of the second-order unification problem
• Title not available (Why is that?)
• The undecidability of \(k\)-provability
• Sets of theorems with short proofs
• A unification algorithm for second-order monadic terms
• Title not available (Why is that?)
• A theorem on generalizations of proofs
• Title not available (Why is that?)
• Some applications of formalized consistency proofs
• Title not available (Why is that?)
• Arithmetic on curves
• Title not available (Why is that?)
• Title not available (Why is that?)
• Recursive Functions of One Variable

Cited In (14)

• Title not available (Why is that?)
• Title not available (Why is that?)
• A theorem on generalizations of proofs
• Taking out LK parts from a proof in Peano arithmetic
• Note on the Benefit of Proof Representations by Name
• Title not available (Why is that?)
• A Proof-theoretic Treatment of Assignments
• Herbrand's theorem and term induction
• Title not available (Why is that?)
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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)