Herbrand's theorem revisited

We present recent results on the deepening connection between proof theory and formal language theory. To each first‐order proof with prenex cuts of complexity at most Π n /Σ n , we associate a typed (non‐deterministic) tree grammar of order n (equivalently, an order n recursion scheme) that abstracts the computation of Herbrand sets obtained through Gentzen‐style cut elimination. Apart from offering a means to compute Herbrand expansions directly from proofs with cuts, these grammars provide a structural counterpart to Herbrand's theorem that opens the door to tackling a number of questions in proof theory such as proof equivalence, proof compression and proof complexity. (© 2016 Wiley‐VCH Verlag GmbH & Co. KGaA, Weinheim)