The Herbrandization of a logical formula (named after Jacques Herbrand

Jacques Herbrand

Jacques Herbrand was a French mathematician who was born in Paris, France and died in La Bérarde, Isère, France. Although he died at only 23 years of age, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse, and Richard Courant.He...

) is a construction that is dual to the Skolemization of a formula. Thoralf Skolem

Thoralf Skolem

Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...

 had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim-Skolem theorem (Skolem 1920). Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem

Herbrand's theorem (proof theory)

Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand . It essentially allows a certain kind of reduction of first-order logic to propositional logic...

 (Herbrand 1930).

The resulting formula is not necessarily equivalent

Logical equivalence

In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...

 to the original one. As with Skolemization which only preserves satisfiability, Herbrandization being Skolemization's dual preserves validity

Validity

In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form is valid....

: the resulting formula is valid if and only if the original one is.

Let be a formula in the language of first-order logic

First-order logic

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate 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. (That is, could be relettered to ensure these conditions, in such a way that the result is an equivalent formula).

The Herbrandization of is then obtained as follows:

• First, replace any free variables in by constant symbols.

• Second, delete all quantifiers on variables that are either (1) universally quantified and within an even number of negation signs, or (2) existentially quantified and within an odd number of negation signs.

• Finally, replace each such variable with a function symbol , where are the variables that are still quantified, and whose quantifiers govern .

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 (since there were no other quantifiers governing ), 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 (1) existentially quantified and within an even number of negations, or (2) 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

Herbrand's theorem (proof theory)

Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand . It essentially allows a certain kind of reduction of first-order logic to propositional logic...

 or the Löwenheim-Skolem theorem.