Herbrand's Theorem - Generalizations of Herbrand's Theorem

Generalizations of Herbrand's Theorem

• Herbrand's theorem has been extended to arbitrary higher-order logics by using expansion-tree proofs. The deep representation of expansion-tree proofs correspond to Herbrand disjunctions, when restricted to first-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 iff it has a Herbrand sequent".