Herbrand's Theorem as Higher Order Recursion

Abstract

We provide a means to compute Herbrand disjunctions directly from sequent calculus proofs with cuts. Our approach associates to a first-order classical proof π + ∃vF, where F is quantifier free, an acyclic higher order recursion scheme H whose language is finite and yields a Herbrand disjunction for ∃vF. More generally, we show that the language of H contains the Herbrand disjunction implicit in any cut-free proof obtained from π via a sequence of Gentzen-style cut reductions that always reduce the weak side of a cut before the strong side.