Herbrandization


The Herbrandization of a logical formula is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim–Skolem theorem. Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem.
The resulting formula is not necessarily equivalent to the original one. As with Skolemization, which only preserves satisfiability, Herbrandization being Skolemization's dual preserves validity: the resulting formula is valid if and only if the original one is.

Definition and examples

Let be a formula in the language of first-order logic. We may assume that contains no variable that is bound by two different quantifier occurrences, and that no variable occurs both bound and free. .
The Herbrandization of is then obtained as follows:
For instance, consider the formula. There are no free variables to replace. The variables are the kind we consider for the second step, so we delete the quantifiers and. Finally, we then replace with a constant , and we replace with a function symbol :
The Skolemization of a formula is obtained similarly, except that in the second step above, we would delete quantifiers on variables that are either existentially quantified and within an even number of negations, or universally quantified and within an odd number of negations. Thus, considering the same from above, its Skolemization would be:
To understand the significance of these constructions, see Herbrand's theorem or the Löwenheim–Skolem theorem.