We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex P2=S2. The representation takes the form of a typed non-deterministic tree grammar G of order 2 which generates a finite language, L(G), of first-order terms that appear in the Herbrand expansions obtained through cut-elimination. In particular, for every Gentzen-style reduction p p 0 between LK-proofs we study the induced grammars, respectively G and G 0 , and classify the cases in which language equality, L(G) = L(G 0 ), and language inclusion, L(G) L(G 0 ), hold.
['Bahareh Afshari', 'Stefan Hetzl', 'Graham E. Leigh']
On the Herbrand content of LK