From Herbrand schemes to functional interpretation

TL;DR

This paper reformulates Herbrand schemes as a functional interpretation of classical sequent calculus, providing a new perspective on extracting logical disjunctions directly from proofs without cut elimination.

Contribution

It introduces a novel reformulation of Herbrand schemes as a functional interpretation, bridging proof extraction methods and functional analysis in logic.

Findings

Herbrand schemes can be viewed as a functional interpretation.

The reformulation aligns Herbrand schemes with existing functional interpretations.

Provides a new framework for proof analysis in classical logic.

Abstract

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.