Editing Skolem normal form (section)

==How Skolemization works==

Skolemization works by applying a [[second-order logic|second-order]] equivalence together with the definition of first-order satisfiability. The equivalence provides a way for "moving" an existential quantifier before a universal one. 

:<math>\forall x   \exists y  R(x,y)  \iff \exists f \forall x  R(x,f(x)) </math>
where
:<math>f(x)</math> is a function that maps <math>x</math> to <math>y</math>.

Intuitively, the sentence "for every <math>x</math> there exists a <math>y</math> such that <math>R(x,y)</math>" is converted into the equivalent form "there exists a function <math>f</math> mapping every <math>x</math> into a <math>y</math> such that, for every <math>x</math> it holds that <math>R(x,f(x))</math>".

This equivalence is useful because the definition of first-order satisfiability implicitly existentially quantifies over functions interpreting the function symbols. In particular, a first-order formula <math>\Phi</math> is satisfiable if there exists a model <math>M</math> and an evaluation <math>\mu</math> of the free variables of the formula that evaluate the formula to ''true''. The model contains the interpretation of all function symbols; therefore, Skolem functions are implicitly existentially quantified. In the example above, <math>\forall x  R(x,f(x))</math> is satisfiable if and only if there exists a model <math>M</math>, which contains an interpretation for <math>f</math>, such that <math>\forall x  R(x,f(x))</math> is true for some evaluation of its free variables (none in this case). This may be expressed in second order as <math>\exists f \forall x  R(x,f(x))</math>. By the above equivalence, this is the same as the satisfiability of <math>\forall x \exists y  R(x,y)</math>.

At the meta-level, [[First-order logic#Semantics|first-order satisfiability]] of a formula <math>\Phi</math> may be written with a little abuse of notation as <math>\exists M \exists \mu  ( M,\mu \models \Phi)</math>, where <math>M</math> is a model, <math>\mu</math> is an evaluation of the free variables, and <math>\models</math> means that <math>\Phi</math> is true in <math>M</math> under <math>\mu</math>. Since first-order models contain the interpretation of all function symbols, any Skolem function that <math>\Phi</math> contains is implicitly existentially quantified by <math>\exists M</math>. As a result, after replacing existential quantifiers over variables by existential quantifiers over functions at the front of the formula, the formula still may be treated as a first-order one by removing these existential quantifiers. This final step of treating <math>\exists f \forall x  R(x,f(x))</math> as <math>\forall x  R(x,f(x))</math> may be completed because functions are implicitly existentially quantified by <math>\exists M</math> in the definition of first-order satisfiability.

Correctness of Skolemization may be shown on the example formula <math>F_1 = \forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)</math> as follows. This formula is satisfied by a [[Model_theory#First-order_logic|model]] <math>M</math> if and only if, for each possible value for <math>x_1,\dots,x_n</math> in the domain of the model, there exists a value for <math>y</math> in the domain of the model that makes <math>R(x_1,\dots,x_n,y)</math> true. By the [[axiom of choice]], there exists a function <math>f</math> such that <math>y = f(x_1,\dots,x_n)</math>. As a result, the formula <math>F_2 = \forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))</math> is satisfiable, because it has the model obtained by adding the interpretation of <math>f</math> to <math>M</math>. This shows that <math>F_1</math> is satisfiable only if <math>F_2</math> is satisfiable as well. Conversely, if <math>F_2</math> is satisfiable, then there exists a model <math>M'</math> that satisfies it; this model includes an interpretation for the function <math>f</math> such that, for every value of <math>x_1,\dots,x_n</math>, the formula <math>R(x_1,\dots,x_n,f(x_1,\dots,x_n))</math> holds. As a result, <math>F_1</math> is satisfied by the same model because one may choose, for every value of <math>x_1,\ldots,x_n</math>, the value <math>y=f(x_1,\dots,x_n)</math>, where <math>f</math> is evaluated according to <math>M'</math>.