The undecidability of \(k\)-provability

DOI10.1016/0168-0072(91)90059-UzbMath0749.03039MaRDI QIDQ1176199

Samuel R. Buss

Publication date: 25 June 1992

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

zbMATH Keywords

sequent calculi\(k\)-provabilityanalysis of formal proofsKreisel conjecturelogic flow graphs

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Complexity of proofs (03F20)

Related Items (24)

Some remarks on lengths of propositional proofs ⋮ On the Power of Substitution in the Calculus of Structures ⋮ Combinatorial flows as bicolored atomic flows ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ Interpolants, cut elimination and flow graphs for the propositional calculus ⋮ Normalization of N-graphs via sub-N-graphs ⋮ Identity of Proofs Based on Normalization and Generality ⋮ A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs ⋮ Asymptotic cyclic expansion and bridge groups of formal proofs ⋮ Paraconsistent informational logic ⋮ Models of deduction ⋮ Cycling in proofs and feasibility ⋮ The Role of Structural Reasoning in the Genesis of Graph Theory ⋮ A unification-theoretic method for investigating the \(k\)-provability problem ⋮ Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic ⋮ Paraconsistent conjectural deduction based on logical entropy measures I: C-systems as non-standard inference framework ⋮ \(k\)-provability in \(\mathrm{PA}\) ⋮ Deep inference and expansion trees for second-order multiplicative linear logic ⋮ Logical structures and genus of proofs ⋮ Maximum segments as natural deduction images of some cuts ⋮ Turning cycles into spirals ⋮ Bounded arithmetic, proof complexity and two papers of Parikh ⋮ Streams and strings in formal proofs.

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• 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
• The undecidability of the second-order unification problem
• 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 +
• A unification-theoretic method for investigating the \(k\)-provability problem
• Sets of theorems with short proofs
• Some Results on the Length of Proofs

This page was built for publication: The undecidability of \(k\)-provability