The Herbrandization of a logical formula (named after Jacques Herbrand) is a construction that is dual to the Skolemization of a formula.
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.
be a formula in the language of first-order logic.
contains no variable that is bound by two different quantifier occurrences, and that no variable occurs both bound and free.
could be relettered to ensure these conditions, in such a way that the result is an equivalent formula).
is then obtained as follows: For instance, consider the formula
There are no free variables to replace.
are the kind we consider for the second step, so we delete the quantifiers
: The Skolemization of a formula is obtained similarly, except that in the second step above, we would delete quantifiers on variables that are either (1) existentially quantified and within an even number of negations, or (2) universally quantified and within an odd number of negations.
from above, its Skolemization would be: To understand the significance of these constructions, see Herbrand's theorem or the Löwenheim–Skolem theorem.