eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2012-09-03
320
334
10.4230/LIPIcs.CSL.2012.320
article
Herbrand-Confluence for Cut Elimination in Classical First Order Logic
Hetzl, Stefan
Straßburger, Lutz
We consider cut-elimination in the sequent calculus for classical
first-order logic. It is well known that this system, in its most
general form, is neither confluent nor strongly normalizing. In this
work we take a coarser (and mathematically more realistic) look at
cut-free proofs. We analyze which witnesses they choose for which
quantifiers, or in other words: we only consider the
Herbrand-disjunction of a cut-free proof. Our main theorem is a
confluence result for a natural class of proofs: all (possibly
infinitely many) normal forms of the non-erasing reduction lead to the
same Herbrand-disjunction.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol016-csl2012/LIPIcs.CSL.2012.320/LIPIcs.CSL.2012.320.pdf
proof theory
first-order logic
tree languages
term rewriting
semantics of proofs