Herbrand Confluence for First-Order Proofs with Π2-Cuts

DOI10.1515/9781501502620-003zbMATH Open1433.03133OpenAlexW2485473430MaRDI QIDQ5221602FDOQ5221602

Graham E. Leigh, Bahareh Afshari, Stefan Hetzl

Publication date: 2 April 2020

Published in: Concepts of Proof in Mathematics, Philosophy, and Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1515/9781501502620-003

Recommendations

• Herbrand-confluence for cut elimination in classical first order logic
• Herbrand's theorem and extractive proof theory
• Proof nets for Herbrand's theorem
• Herbrand's theorem, Skolemization and proof systems for first-order Łukasiewicz logic
• Herbrand's theorem for prenex Gödel logic and its consequences for theorem proving
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• scientific article; zbMATH DE number 3296226
• Lower and upper bounds for the provability of Herbrand consistency in weak arithmetics
• scientific article
• Gentzen's second consistency proof and strong cut-elimination

zbMATH Keywords

first-order logicHerbrand's theoremcut eliminationformal language theory

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42) Structure of proofs (03F07)

Cited In (5)

• Herbrand's theorem as higher order recursion
• The \(\exists\forall^2\) fragment of the first-order theory of atomic set constraints is \(\Pi_1^0\)-hard
• On the Herbrand content of LK
• On the generation of quantified lemmas
• On the compressibility of finite languages and formal proofs

This page was built for publication: Herbrand Confluence for First-Order Proofs with Π₂-Cuts

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