Skolemization is the process of:

Concept

In first-order logic, Skolemization transforms a formula into an equisatisfiable formula by eliminating existential quantifiers.

Each existential variable is replaced by a fresh Skolem constant when it depends on no universal variable, or by a Skolem function of the universally quantified variables in whose scope it occurs.

Application

1. Start with ∀x ∃y P(x, y).

2. Because y is within the scope of ∀x, replace y by a fresh Skolem function f(x).

3. The result is ∀x P(x, f(x)): the existential quantifier is gone, while the universal quantifier remains.

Contrast

• Bringing all quantifiers to the front is conversion to prenex normal form.

• Universal quantifiers represent arbitrary variables and are not the quantifiers eliminated by Skolemization.

• Bringing quantifiers to the front and eliminating universal and existential quantifiers are distinct transformations; they do not all share the name Skolemization.

Cross-check

The transformed formula contains no existential quantifier and remains equisatisfiable with the original formula, which is the defining objective of Skolemization.

Therefore, Skolemization is the process of removing existential quantifiers through suitable Skolem terms.