Herbrand-Confluence for Cut Elimination in Classical First Order Logic
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.
proof theory
first-order logic
tree languages
term rewriting
semantics of proofs
320-334
Regular Paper
Stefan
Hetzl
Stefan Hetzl
Lutz
Straßburger
Lutz Straßburger
10.4230/LIPIcs.CSL.2012.320
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode