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.

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

<math>\forall x_1 \dots \forall x_n \exists y M(x_1,\dots,x_n,y)<math>

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

<math>x_1,\dots,x_n<math>

which makes

<math>M(x_1,\dots,x_n,y)<math>

true, and there will be some function

<math>y = f(x_1,\dots,x_n)<math>

which makes the formula

<math>\forall x_1 \dots \forall x_n M(x_1,\dots,x_n,f(x_1,\dots,x_n))<math>

hold in this model.

The function f is called a Skolem function.