Herbrand's theorem has been extended to by using expansion-tree proofs.[3] The deep representation of expansion-tree proofs corresponds to a Herbrand disjunction, when restricted to first-order logic.

higher-order 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 if and only if it has a Herbrand sequent".

Herbrand structure

Herbrand interpretation

Herbrand universe

Compactness theorem

(1995), "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël (eds.), Logic and Computational Complexity, Lecture Notes in Computer Science, Berlin, New York: Springer-Verlag, pp. 195–209, ISBN 978-3-540-60178-4.

Buss, Samuel R.