Skolem normal form
From Free net encyclopedia
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
- <math>\forall x \exists y R(x,y) \Leftrightarrow \exists f \forall x R(x,f(x))</math>
The essence of Skolemization is the observation that if a formula in the form
- <math>\forall x_1 \dots \forall x_n \exists y R(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>R(x_1,\dots,x_n,y)</math>
true, and there must exist some function (assuming choice)
- <math>y = f(x_1,\dots,x_n)</math>
which makes the formula
- <math>\forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))</math>
true. The function f is called a Skolem function.
[edit]
See also
[edit]
