Herbrand’s Theorem as Higher Order Recursion

View/ Open
Date
2018-02-19MFO Scientific Program
Research in Pairs 2016Series
Oberwolfach Preprints;2018,01Author
Afshari, Bahareh
Hetzl, Stefan
Leigh, Graham E.
Metadata
Show full item recordOWP-2018-01
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 $\pi \vdash \exists v F$, where $F$ is quantifier free, an acyclic higher order recursion scheme $\mathscr H$ whose language is finite and yields a Herbrand disjunction for $\exists v F$. More generally, we show that the language of $\mathscr H$ contains the Herbrand disjunction implicit in any cut-free proof obtained from $\pi$ via a sequence of Gentzen-style cut reductions that always reduce the weak side of a cut before the strong side.