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 yM(x,y)\Leftrightarrow \exists f\forall xM(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 yM(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.

External links

• Skolemization on PlanetMath.org