Herbrand-confluence (Q2871477)

One of the important problems of proof theory as well as of computer science is that of the constructive content of a proof. In classical logic, a single proof allows different constructive meanings which, in terms of applications means that different programs can be extracted from it. This phenomenon in the setting of sequent calculus is represented by the fact that standard proof of cut elimination is not confluent.NEWLINENEWLINEIn order to compare cut-free proofs obtained from the proof (with cuts) in sequent calculus for classical logic, the authors introduce the notion of equivalence of proofs based on Herbrand disjunctions. A non-erasing cut-reduction relation is Herbrand-confluent if all its normal forms have the same Herbrand disjunctions. The main result of the paper is Herbrand-confluence theorem for some class of proofs called simple. In simple proofs, every cut-formula is either quantifier-free or with only one quantifier as the main constant. It appears that normal proofs of arbitrary size in this class are equivalent in this sense.NEWLINENEWLINEThe main technique used for proving this result is the application of rigid tree languages which are associated with proofs. In such setting, a Herbrand-content of a proof may be defined as the language of the grammar of this proof. This approach allows also for a combinatorial description of the relation between a proof and its cut-free version. The result is first established for proofs with skolemized end-sequents, and then extended to the general case.