Skolem normal form

From Wikipedia, the free encyclopedia

A formula of first-order logic is in Skolem normal form (named after Thoralf Skolem) if its prenex normal form only contains universal quantifiers. Every first-order formula can be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization. The resulting formula is not necessarily equivalent to the original one, but is satisfiable if and only if the original one is.

Skolemization is performed by replacing every existentially quantified variable $y$ with a term $f(x_1,\ldots,x_n)$ whose function symbol $f$ is new (does not occur anywhere else in the formula.) The variables of this term are as follows. If the formula is in prenex normal form, $x_1,\ldots,x_n$ are the variables that are universally quantified and whose quantifiers preceed that of $y$ . In general, they are the variables that are universally quantified and such that $\exists y$ occurs in the scope of their quantifiers. The function $f$ introduced in this process is called Skolem function and the term is called Skolem term.

As an example, the formula $\forall x \exists y \forall z. P(x,y,z)$ is not in Skolem normal form because it contains the existential quantifier $\exists y$ . Skolemization replaces $y$ with $f (x)$ , where $f$ is a new function symbol, and removes the quantification over $y$ . The resulting formula is $\forall x \forall z . P(x,f(x),z)$ . The Skolem term $f (x)$ contains $x$ but not $z$ because the quantifier to be removed $\exists y$ is in the scope of $\forall x$ but not in that of $\forall z$ ; since this formula is in prenex normal form, this is equivalent to saying that $x$ preceeds $y$ while $z$ does not. The formula obtained by this transformation is satisfiable if and only if the original formula is.

1 How Skolemization works
2 Uses of Skolemization
3 Skolem theories
4 References
5 See also
6 External links

[edit] How Skolemization works

Skolemization works by applying a second-order equivalence in conjunction to the definition of first-order satisfaibility. The equivalence provides a way for "moving" an existential quantifier before a universal one.

$\forall x \exists y . R(x,y) \iff \exists f \forall x . R(x,f(x))\mbox{.}$

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

This equivalence is useful because the definition of first-order satisfiability implicitely existentially quantifies over the evaluation of function symbols. In particular, a first-order formula $Φ$ is satisfiable if there exists a model $M$ such that, for every evaluation $μ$ of the free variabiles of the formula, the formula evaluates to true. Since the model contains the evaluation of all function symbols, every Skolem functions is implicitely existentially quantified. In the example above, $\forall x . R(x,f(x))$ is satisfiable if and only if there exists a model $M$ , which contains an evaluation for $f$ , such that $\forall x . R(x,f(x))$ is true for every possible evaluation of its free variables (none in this case). This can be expressed in second order as $\exists f \forall x . R(x,f(x))$ . By the above equivalence, this is the same as the satisfiability of $\forall x \exists y . R(x,y)$ .

At the meta-level, first-order satisfiability can be written as $\exists M \forall \mu ~.~ ( M,\mu \models \Phi )$ , where $M$ is a model and $μ$ is a variable evaluation. Since first-order models contain the evaluation of all function symbol, any Skolem function $Φ$ contains is implicitely existentially quantified by $\exists M$ . As a result, after replacing the existential quantifier over variabiles into existential quantifiers over functions at the front of the formula, the formula can still be treated as a first-order one by removing these existential quantifiers. This final step of treating $\exists f \forall x . R(x,f(x))$ as $\forall x . R(x,f(x))$ can be done because functions are implicitely existentially quantified in the quantifier $\exists M$ of the definition of first-order satisfiability.

Correctness of Skolemization is shown on the example formula $F_1 = \forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)$ . This formula is satisfied by a model $M$ if and only if, for each possible value for $x_1,\dots,x_n$ in the model there exists a value for $y$ in the model that makes $R(x_1,\dots,x_n,y)$ true. By the axiom of choice, there exists a function $f$ such that $y = f(x_1,\dots,x_n)$ . As a result, the formula $F_2 = \forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))$ is satisfiable, because it has the model obtained by adding the evaluation of $f$ to $M$ . This shows that $F 1$ is satisfiable only if $F 2$ is satisfiabile as well. In the other way around, if $F 2$ is satisfiable, then there exists a model $M'$ that satisfies it; this model includes an evaluation for the function $f$ such that, for every value of $x_1,\dots,x_n$ , the formula $R(x_1,\dots,x_n,f(x_1,\dots,x_n))$ holds. As a result, $F 1$ is satisfied by the same model because one can choose, for every value of $x_1,\ldots,x_n$ , the value $y=f(x_1,\dots,x_n)$ , where $f$ is evaluated according to $M'$ .

[edit] Uses of Skolemization

Please help improve this article by expanding this section.
Further information might be found on the talk page or at requests for expansion. Please remove this message once the section has been expanded.

One of the uses of Skolemization is automated theorem proving. For example, in the method of analytic tableaux, whenever a formula whose leading quantifier is existential occurs, the formula obtained by removing that quantifier via Skolemization can be generated. For example, if $\exists x . \Phi(x,y_1,\ldots,y_n)$ occurs in a tableau, where $x,y_1,\ldots,y_n$ are the free variables of $\Phi(x,y_1,\ldots,y_n)$ , then $\Phi(f(y_1,\ldots,y_n),y_1,\ldots,y_n)$ can be added to the same branch of the tableau. This addition does not alter the satisfiability of the tableau: every model of the old formula can be extended, by adding it a suitable evaluation of $f$ , to a model of the new formula.

This form of Skolemization is actually an improvement over "classical" Skolemization in that only variables that are free in the formula are placed in the Skolem term. This is an improvement because the semantics of tableau may implicitely place the formula in the scope of some universally quantified variables that are not in the formula itself; these variables are not in the Skolem term, while they would be there according to the original definition of Skolemization. Another improvement that can be used is using the same Skolem function symbol for formulae that are identical up to variable renaming ^[1].

[edit] Skolem theories

In general, if $T$ is a theory and for each formula $F$ with free variables $x_1, \dots, x_n, y$ there is a Skolem function, then $T$ is called a Skolem theory.[1] For example, by the above, arithmetic with the Axiom of Choice is a Skolem theory.