Skolem normal form
Encyclopedia
Reduction to Skolem normal form is a method for removing existential quantifiers
from formal logic
statements, often performed as the first step in an automated theorem prover.
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 (sometimes spelled "Skolemnization"). 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 satisfiable.
The simplest form of Skolemization is for existentially quantified variables which are not inside the scope of a universal quantifier. 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, 
precedes 
while 
does not. The formula obtained by this transformation is satisfiable if and only if the original formula is.
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 to 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 symbols, 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 
.
. 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 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.
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, arithmetic
with the Axiom of Choice is a Skolem theory.
Every Skolem theory is model complete
, i.e. every substructure
of a model is an elementary substructure
. Given a model M of a Skolem theory T, the smallest substructure containing a certain set A is called the Skolem hull of A. The Skolem hull of A is an atomic prime model
over A.
Existential quantification
In predicate logic, an existential quantification is the predication of a property or relation to at least one member of the domain. It is denoted by the logical operator symbol ∃ , which is called the existential quantifier...
from formal logic
Formal logic
Classical or traditional system of determining the validity or invalidity of a conclusion deduced from two or more statements...
statements, often performed as the first step in an automated theorem prover.
A formula
Formula
In mathematics, a formula is an entity constructed using the symbols and formation rules of a given logical language....
of first-order logic
First-order logic
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...
is in Skolem normal form (named after Thoralf Skolem
Thoralf Skolem
Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
) if it is in conjunctive prenex normal form
Prenex normal form
A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers followed by a quantifier-free part .Every formula in classical logic is equivalent to a formula in prenex normal form...
with only universal first-order quantifiers
Universal quantification
In predicate logic, universal quantification formalizes the notion that something is true for everything, or every relevant thing....
. Every first-order formula can be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled "Skolemnization"). The resulting formula is not necessarily equivalent
Logical equivalence
In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...
to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.
The simplest form of Skolemization is for existentially quantified variables which are not inside the scope of a universal quantifier. 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 formPrenex normal form
A formula of the predicate calculus is in prenex normal form if it is written as a string of quantifiers followed by a quantifier-free part .Every formula in classical logic is equivalent to a formula 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 arityArity
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the dimension of the domain in the corresponding Cartesian product...
) 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, precedes 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-orderSecond-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
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 to 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 symbols, 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 provingAutomated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
. For example, in the method of analytic tableaux
Method of analytic tableaux
In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure...
, 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 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
Scope (programming)
In computer programming, scope is an enclosing context where values and expressions are associated. Various programming languages have various types of scopes. The type of scope determines what kind of entities it can contain and how it affects them—or semantics...
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
Up to
In mathematics, the phrase "up to x" means "disregarding a possible difference in x".For instance, when calculating an indefinite integral, one could say that the solution is f "up to addition by a constant," meaning it differs from f, if at all, only by some constant.It indicates that...
variable renaming.
Skolem theories
In general, if is a theoryTheory (mathematical logic)
In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
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, arithmeticArithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
with the Axiom of Choice is a Skolem theory.
Every Skolem theory is model complete
Model complete theory
In model theory, a first-order theory is called model complete if every embedding of models is an elementary embedding.Equivalently, every first-order formula is equivalent to a universal formula.This notion was introduced by Abraham Robinson....
, i.e. every substructure
Substructure
In mathematical logic, an substructure or subalgebra is a structure whose domain is a subset of that of a bigger structure, and whose functions and relations are the traces of the functions and relations of the bigger structure...
of a model is an elementary substructure
Elementary equivalence
In model theory, a field within mathematical logic, two structures M and N of the same signature σ are called elementarily equivalent if they satisfy the same first-order σ-sentences....
. Given a model M of a Skolem theory T, the smallest substructure containing a certain set A is called the Skolem hull of A. The Skolem hull of A is an atomic prime model
Prime model
In mathematics, and in particular model theory, a prime model is a model which is as simple as possible. Specifically, a model P is prime if it admits an elementary embedding into any model M to which it is elementarily equivalent .- Cardinality :In contrast with the notion of saturated model,...
over A.
See also
- Resolution (logic)Resolution (logic)In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic...
- Method of analytic tableauxMethod of analytic tableauxIn proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure...
- HerbrandizationHerbrandizationThe Herbrandization of a logical formula is a construction that is dual to the Skolemization of a formula. Thoralf Skolem had considered the Skolemizations of formulas in prenex form as part of his proof of the Löwenheim-Skolem theorem...
- Predicate functor logicPredicate functor logicIn mathematical logic, predicate functor logic is one of several ways to express first-order logic by purely algebraic means, i.e., without quantified variables. PFL employs a small number of algebraic devices called predicate functors that operate on terms to yield terms...
External links
- Skolemization on PlanetMath.org
- Skolemization by Hector Zenil, The Wolfram Demonstrations Project.