Herbrand-Confluence
Logic in Computer Science
2016-03-27 v2
Abstract
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.
Cite
@article{arxiv.1310.8156,
title = {Herbrand-Confluence},
author = {Stefan Hetzl and Lutz Straßburger},
journal= {arXiv preprint arXiv:1310.8156},
year = {2016}
}
Comments
25 pages, final version, accepted for publication at LMCS, special issue for CSL 2012