Skolem normal form

Skolem normal form

A formula of first-order logic is in Skolem normal form (named after Thoralf Skolem) if it is in conjunctive prenex normal form with only universal first-order 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 equisatisfiable with 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, exists x P(x) can be changed to "P(c)", where "c" is a new constant.

More generally, 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 precede 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 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 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, in the list of quantifers, x precede y while z 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.

:forall x Big( g(x) vee exists y R(x,y) Big) iff forall x Big( g(x) vee R(x,f(x)) Big)where:f(x) 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 Phi is satisfiable if there exists a model M and an evaluation mu 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, 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 some 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 of a formula Phi can be written with a little abuse of notation as exists M exists mu ~.~ ( M,mu models Phi), where M is a model and mu is an evaluation of the free variables. Since first-order models contain the evaluation of all function symbol, any Skolem function Phi contains is implicitly existentially quantified by exists M. 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 exists f forall x . R(x,f(x)) as forall x . R(x,f(x)) can be done because functions are implicitly existentially quantified by exists M in the definition of first-order satisfiability.

Correctness of Skolemization can be shown on the example formula F_1 = forall x_1 dots forall x_n exists y R(x_1,dots,x_n,y) as follows. This formula is satisfied by a model M if and only if, for each possible value for x_1,dots,x_n in the domain of the model there exists a value for y in the domain of 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 satisfiable 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'.

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 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 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.] .

kolem 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. [http://www.math.uu.nl/people/jvoosten/syllabi/logicasyllmoeder.pdf] For example, by the above, arithmetic with the Axiom of Choice is a Skolem theory.

References

ee also

* Resolution (logic)
* Method of analytic tableaux
* Herbrandization

External links

* [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.

Look at other dictionaries:

  • Skolem normal form — A formula is in Skolem normal form if it is in prenex normal form, and all the existential quantifiers come first. There is an effective procedure producing, for any formula, one in Skolem normal form that is valid if and only if the original is… …   Philosophy dictionary

  • Normal form — may refer to: Normal form (abstract rewriting) Normal form (databases) Normal form (game theory) Normal form (mathematics) In formal language theory: Beta normal form Chomsky normal form Greibach normal form Kuroda normal form Normal form… …   Wikipedia

  • Clausal normal form — The clausal normal form (or clause normal form, conjunctive normal form, CNF) of a logical formula is used in logic programming and many theorem proving systems. A formula in clause normal form is a set of clauses, interpreted as a conjunction. A …   Wikipedia

  • Löwenheim–Skolem theorem — In mathematical logic, the Löwenheim–Skolem theorem, named for Leopold Löwenheim and Thoralf Skolem, states that if a countable first order theory has an infinite model, then for every infinite cardinal number κ it has a model of size κ. The… …   Wikipedia

  • Thoralf Skolem — Infobox Scientist name = Thoralf Skolem birth date = birth date|1887|5|23|mf=y birth place = Sandsvaer, Buskerud, Norway residence = nationality = death date = death date and age|1963|3|23|1887|5|23|mf=y death place = Oslo, Norway field =… …   Wikipedia

  • Canonical form — Generally, in mathematics, a canonical form (often called normal form or standard form) of an object is a standard way of presenting that object. Canonical form can also mean a differential form that is defined in a natural (canonical) way; see… …   Wikipedia

  • First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… …   Wikipedia

  • List of mathematics articles (S) — NOTOC S S duality S matrix S plane S transform S unit S.O.S. Mathematics SA subgroup Saccheri quadrilateral Sacks spiral Sacred geometry Saddle node bifurcation Saddle point Saddle surface Sadleirian Professor of Pure Mathematics Safe prime Safe… …   Wikipedia

  • List of philosophy topics (R-Z) — RRaRabad Rabbinic law Rabbinic theology Francois Rabelais François Rabelais race racetrack paradox racism Gustav Radbruch Janet Radcliffe Richards Sarvepalli Radhakrishnan radical Aristotelianism radical behaviourism radical feminism radical… …   Wikipedia

  • List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”