Handbook of Automated Reasoning

By Herbrand's theorem, every valid sequent containing weak quantifiers only defines a corresponding Herbrand sequent; thus, Herbrand complexity is well-defined. Still, $\mathcal{H}\mathcal{C}$ can be defined in several ways—depending on our choice of a complexity measure for sequents (an alternative would be to define ‖S‖ as the number of symbol occurrences in the sequent S). As skolemization is a method of removing strong quantifiers, any sequent resulting from a valid one has a Herbrand complexity. The following theorem shows that different forms of skolemization may yield sequents with strongly different Herbrand complexity.

5.16. Theorem.

There exists ...