ABSTRACT. Herbrand's Theorem, a fundamental result of classical logic, states that for every valid existential formula $ \exists x F(x) $ there is a finite set of terms $ T $ such that the quantifier-free disjunction $ \bigvee_{t\in T} F(t) $ is a tautology. Herbrand disjunctions can be computed in a number of ways, such as via cut-elimination, re-interpretations of classical logic in intuitionistic logic and term calculi for classical natural deduction.

In this talk I will outline a language-theoretic representation of Herbrand's Theorem. Specifically, I will introduce a class of higher order recursion schemes (HORS) for computing Herbrand disjunctions from classical sequent calculus proofs. HORS are a generalisation of regular tree grammars to finite types which equate to the simply-typed $\lambda Y$-calculus with non-deterministic reductions. The representation interprets inference rules of proofs as non-terminals whose production rules operate compositionally to extract the term instantiations that result from reductive cut-elimination. Current limitations of the approach, as well as future directions, will be discussed.