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

Related Topics:
Formula - First-order logic - Prenex normal form - Equisatisfiable - Second-order

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:orall x exists y M(x,y) Leftrightarrow exists f orall x M(x,f(x))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:orall x_1 dots orall 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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:orall x_1 dots orall x_n M(x_1,dots,x_n,f(x_1,dots,x_n))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The function f is called a Skolem function.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~