Skolem normal form

A formula of first-order logic is in Skolem normal form if its prenex normal form has only universal quantifiers. A formula can be Skolemized, that is have its existential quantifiers eliminated to produce an equisatisfiable formula to the original. Skolemization is an application of the (second-order) equivalence

$\forall x \exists y M(x,y) \Leftrightarrow \exists f \forall x M(x,f(x))$

The essence of skolemization is the observation that if a formula in the form

$\forall x_1 \dots \forall x_n \exists y M(x_1,\dots,x_n,y)$

is satisfiable in some model, then there must be some point in the model for every

$x_1,\dots,x_n$

which makes

$M(x_1,\dots,x_n,y)$

true, and there must exist some function

$y = f(x_1,\dots,x_n)$

which makes the formula

$\forall x_1 \dots \forall x_n M(x_1,\dots,x_n,f(x_1,\dots,x_n))$

The function f is called a Skolem function.

This mathematics-related article is a stub. You can help Wikipedia by expanding it.

See also: Skolem normal form, First-order logic, Formula, Mathematics, Model, Prenex normal form, Second-order logic, Skolem function