The article presents a method for computing Herbrand expansions from derivations in a standard classical sequent calculus for predicate logic through recursion schemes. The aim of the authors is of creating a method for extracting computational content without first requiring cut elimination. Other methods for this include Hilbert’s \(\epsilon\)-calculus, variants of Gödel’s functional interpretation, and so on. The follow-up questions of the authors are; (1) which Herbrand expansions can be computed from a derivation without eliminating cut, and (2) what is the minimal amount of information needed to describe these expansions? The answer is given through a definition of higher-order recursion schemes. The authors describe the higher order recursion schemes presented in Section 3.2 as “a generalisation of regular and context-free grammars to the simple type hierarchy”.
The article’s main result is Theorem 1.1 that proves a bound for the size of the language of the Herbrand expansions. A comparison of the bound to similar results such as [P. Gerhardy and U. Kohlenbach, Arch. Math. Log. 44, No 5, 633–644 (2005; Zbl 1082.03056); S. Buss, in: Gentzen’s centenary. The quest for consistency. Cham: Springer. 245–277 (2015; Zbl 1380.03062)] is found in Section 8. The article also contains an application of the method in Section 5: a case study that analyses the Herbrand expansions for a proof of the pigeonhole principle.