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
- <math>\forall x \exists y M(x,y) \Leftrightarrow \exists f \forall x M(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 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 must exist 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>
The function f is called a Skolem function.