logic. Herbrand disjunctions and expansion-tree proofs have been extended with a notion of cut. Due to the complexity of cut-elimination, Herbrand disjunctions with cuts can be non-elementarily smaller than a standard Herbrand disjunction. Herbrand disjunctions have been generalized to Herbrand sequents, allowing Herbrand's theorem to be stated for sequents: "a Skolemized sequent is derivable iff it has a Herbrand sequent". See also Herbrand structure Herbrand interpretation Herbrand universe Compactness theorem Notes References . Proof theory Theorems in the foundations of mathematics Metatheorems