Herbrand's theorem

Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic,[2] the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular.

This version of Herbrand's theorem states that the above formula is valid if and only if there exists a finite sequence of terms

in prenex form containing only existential quantifiers is provable (valid) in first-order logic if and only if a disjunction composed of substitution instances of the quantifier-free subformula of

The restriction to formulas in prenex form containing only existential quantifiers does not limit the generality of the theorem, because formulas can be converted to prenex form and their universal quantifiers can be removed by Herbrandization.

Conversion to prenex form can be avoided, if structural Herbrandization is performed.