From Herbrand schemes to functional interpretation
This work provides a theoretical reformulation for proof theory researchers, but it appears incremental as it adapts known ideas to a specific context.
The paper reformulates Herbrand schemes, a method for extracting Herbrand disjunctions from sequent calculus proofs without cut elimination, as a functional interpretation of classical sequent calculus, similar to existing interpretations by Gerhardy and Kohlenbach.
Herbrand schemes are a method to extract Herband disjunctions directly from sequent calculus proofs, without appealing to cut elimination, using a formal grammar known as a higher-order recursion scheme. In this note, we show that the core ideas of Herbrand schemes can be reformulated as a functional interpretation of classical sequent calculus, similar to the functional interpretation of classical logic due to Gerhardy and Kohlenbach.