Herbrand's theorem as higher order recursion (Q1987218): Difference between revisions

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 [\textit{P. Gerhardy} and \textit{U. Kohlenbach}, Arch. Math. Log. 44, No 5, 633--644 (2005; Zbl 1082.03056); \textit{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.