A sequent calculus demonstration of Herbrand's theorem

TL;DR

This paper provides a rigorous sequent calculus proof of Herbrand's theorem in full generality, addressing previous gaps by demonstrating the admissibility of deep contraction to ensure completeness.

Contribution

It offers a correct, comprehensive proof of Herbrand's theorem using sequent calculus, correcting prior flawed approaches and extending the theorem's applicability.

Findings

Established the admissibility of deep contraction in sequent calculus

Provided a complete proof of Herbrand's theorem in full generality

Addressed and fixed flaws in previous proofs

Abstract

Herbrand's theorem is often presented as a corollary of Gentzen's sharpened Hauptsatz for the classical sequent calculus. However, the midsequent gives Herbrand's theorem directly only for formulae in prenex normal form. In the Handbook of Proof Theory, Buss claims to give a proof of the full statement of the theorem, using sequent calculus methods to show completeness of a calculus of Herbrand proofs, but as we demonstrate there is a flaw in the proof. In this note we give a correct demonstration of Herbrand's theorem in its full generality, as a corollary of the full cut-elimination theorem for LK. The major difficulty is to show that, if there is an Herbrand proof of the premiss of a contraction rule, there is an Herbrand proof of its conclusion. We solve this problem by showing the admissibility of a deep contraction rule.