Skolem normal form

In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers.

Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization).

[1] Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover.

The simplest form of Skolemization is for existentially quantified variables that are not inside the scope of a universal quantifier.

These may be replaced simply by creating new constants.

More generally, Skolemization is performed by replacing every existentially quantified variable

If the formula is in prenex normal form, then

is not in Skolem normal form because it contains the existential quantifier

is a new function symbol, and removes the quantification over

; since this formula is in prenex normal form, this is equivalent to saying that, in the list of quantifiers,

Skolemization works by applying a second-order equivalence together with the definition of first-order satisfiability.

The equivalence provides a way for "moving" an existential quantifier before a universal one.

" is converted into the equivalent form "there exists a function

This equivalence is useful because the definition of first-order satisfiability implicitly existentially quantifies over functions interpreting the function symbols.

is true for some evaluation of its free variables (none in this case).

At the meta-level, first-order satisfiability of a formula

As a result, after replacing existential quantifiers over variables by existential quantifiers over functions at the front of the formula, the formula still may be treated as a first-order one by removing these existential quantifiers.

may be completed because functions are implicitly existentially quantified by

Correctness of Skolemization may be shown on the example formula

By the axiom of choice, there exists a function

is satisfiable, because it has the model obtained by adding the interpretation of

that satisfies it; this model includes an interpretation for the function

One of the uses of Skolemization is within automated theorem proving.

For example, in the method of analytic tableaux, whenever a formula whose leading quantifier is existential occurs, the formula obtained by removing that quantifier via Skolemization may be generated.

This addition does not alter the satisfiability of the tableau: every model of the old formula may be extended, by adding a suitable interpretation of

This is an improvement because the semantics of tableaux may implicitly place the formula in the scope of some universally quantified variables that are not in the formula itself; these variables are not in the Skolem term, while they would be there according to the original definition of Skolemization.

Another improvement that may be used is applying the same Skolem function symbol for formulae that are identical up to variable renaming.

[2] Another use is in the resolution method for first-order logic, where formulas are represented as sets of clauses understood to be universally quantified.

An important result in model theory is the Löwenheim–Skolem theorem, which can be proven via Skolemizing the theory and closing under the resulting Skolem functions.

is a theory and for each formula with free variables