- Skolem normal form
formulaof first-order logicis in Skolem normal form (named after Thoralf Skolem) if it is in conjunctive prenex normal formwith only universal first-order quantifiers. Every first-order formula can be converted into Skolem normal form while not changing its satisfiabilityvia a process called Skolemization. The resulting formula is not necessarily equivalent to the original one, but is equisatisfiablewith it: it is satisfiable if and only if the original one is. The simplest form of Skolemization is for existentially quantified variables which are not inside the scope of a universal quantifiers. These can simply be replaced by creating new constants. For example, can be changed to "P(c)", where "c" is a new constant.
More generally, Skolemization is performed by replacing every existentially quantified variable with a term whose function symbol 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, are the variables that are universally quantified and whose quantifiers precede that of . In general, they are the variables that are universally quantified and such that occurs in the scope of their quantifiers. The function introduced in this process is called a Skolem function (or Skolem constant if it is of zero arity) and the term is called a Skolem term. As an example, the formula is not in Skolem normal form because it contains the existential quantifier . Skolemization replaces with , where is a new function symbol, and removes the quantification over . The resulting formula is . The Skolem term contains but not because the quantifier to be removed is in the scope of but not in that of ; since this formula is in prenex normal form, this is equivalent to saying that, in the list of quantifers, precede while does not. The formula obtained by this transformation is satisfiable if and only if the original formula is.
How Skolemization works
Skolemization works by applying a second-order equivalence in conjunction to the definition of first-order satisfiability. The equivalence provides a way for "moving" an existential quantifier before a universal one.
:where: is a function that maps x into y.
Intuitively, the sentence "for every x there exists a y such that R(x,y)" is converted into the equivalent form "there exists a function f mapping every x into a y such that, for every x it holds R(x,f(x))".
This equivalence is useful because the definition of first-order satisfiability implicitly existentially quantifies over the evaluation of function symbols. In particular, a first-order formula is satisfiable if there exists a model and an evaluation of the free variables of the formula that evaluate the formula to "true". The model contains the evaluation of all function symbols; therefore, Skolem functions are implicitly existentially quantified. In the example above, is satisfiable if and only if there exists a model , which contains an evaluation for , such that is true for some evaluation of its free variables (none in this case). This can be expressed in second order as . By the above equivalence, this is the same as the satisfiability of .
At the meta-level, first-order satisfiability of a formula can be written with a little abuse of notation as , where is a model and is an evaluation of the free variables. Since first-order models contain the evaluation of all function symbol, any Skolem function contains is implicitly existentially quantified by . As a result, after replacing an existential quantifier over variables into an 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 as can be done because functions are implicitly existentially quantified by in the definition of first-order satisfiability.
Correctness of Skolemization can be shown on the example formula as follows. This formula is satisfied by a model if and only if, for each possible value for in the domain of the model there exists a value for in the domain of the model that makes true. By the
axiom of choice, there exists a function such that . As a result, the formula is satisfiable, because it has the model obtained by adding the evaluation of to . This shows that is satisfiable only if is satisfiable as well. In the other way around, if is satisfiable, then there exists a model that satisfies it; this model includes an evaluation for the function such that, for every value of , the formula holds. As a result, is satisfied by the same model because one can choose, for every value of , the value , where is evaluated according to .
Uses of Skolemization
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 occurs in a tableau, where are the free variables of , then 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 , 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 implicitly 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 [R. Hänle. Tableaux and related methods.
Handbook of Automated Reasoning.] .
In general, if is a theory and for each formula with
free variables there is a Skolem function, then is called a Skolem theory. [http://www.math.uu.nl/people/jvoosten/syllabi/logicasyllmoeder.pdf] For example, by the above, arithmeticwith the Axiom of Choice is a Skolem theory.
Method of analytic tableaux
* [http://planetmath.org/encyclopedia/Skolemization.html Skolemization on PlanetMath.org]
* [http://demonstrations.wolfram.com/Skolemization/ Skolemization] by Hector Zenil,
The Wolfram Demonstrations Project.
Wikimedia Foundation. 2010.