|
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. Put together, this is
- <math>\exists f \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.
|
