Skolem normal form – Wikipedia
Formalism of first-order logic
In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers.
Every first-order formula may 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.[1]
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.
Examples[edit]
The simplest form of Skolemization is for existentially quantified variables that are not inside the scope of a universal quantifier. These may be replaced simply by creating new constants. For example,
∃xP(x){displaystyle exists xP(x)}may be changed to
c{displaystyle c} , where
is a new constant (does not occur anywhere else in the formula).
More generally, Skolemization is performed by replacing every existentially quantified variable
y{displaystyle y}f(x1,…,xn){displaystyle f(x_{1},ldots ,x_{n})} with a term
f{displaystyle f} whose function symbol
x1,…,xn{displaystyle x_{1},ldots ,x_{n}} is new. The variables of this term are as follows. If the formula is in prenex normal form, then
y{displaystyle y} are the variables that are universally quantified and whose quantifiers precede that of
∃y{displaystyle exists y} . In general, they are the variables that are quantified universally (we assume we get rid of existential quantifiers in order, so all existential quantifiers before
∃y{displaystyle exists y} have been removed) and such that
f{displaystyle f} 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
∀x∃y∀z.P(x,y,z){displaystyle forall xexists yforall z.P(x,y,z)}∃y{displaystyle exists y} is not in Skolem normal form because it contains the existential quantifier
y{displaystyle y} . Skolemization replaces
f(x){displaystyle f(x)} with
f{displaystyle f} , where
y{displaystyle y} is a new function symbol, and removes the quantification over
∀x∀z.P(x,f(x),z){displaystyle forall xforall z.P(x,f(x),z)} . The resulting formula is
f(x){displaystyle f(x)} . The Skolem term
x{displaystyle x} contains
z{displaystyle z} , but not
∃y{displaystyle exists y} , because the quantifier to be removed
∀x{displaystyle forall x} is in the scope of
∀z{displaystyle forall z} , but not in that of
x{displaystyle x} ; since this formula is in prenex normal form, this is equivalent to saying that, in the list of quantifiers,
y{displaystyle y} precedes
z{displaystyle z} while
does not. The formula obtained by this transformation is satisfiable if and only if the original formula is.
How Skolemization works[edit]
Skolemization works by applying a 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.
- ∀x∃yR(x,y)⟺∃f∀xR(x,f(x)){displaystyle forall xexists yR(x,y)iff exists fforall xR(x,f(x))}
where
- f(x){displaystyle f(x)} is a function that maps x{displaystyle x} to y{displaystyle y} .
Intuitively, the sentence “for every
x{displaystyle x}y{displaystyle y} there exists a
R(x,y){displaystyle R(x,y)} such that
f{displaystyle f} ” is converted into the equivalent form “there exists a function
x{displaystyle x} mapping every
y{displaystyle y} into a
x{displaystyle x} such that, for every
R(x,f(x)){displaystyle R(x,f(x))} it holds
“.
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
Φ{displaystyle Phi }M{displaystyle M} is satisfiable if there exists a model
μ{displaystyle mu } and an evaluation
∀x.R(x,f(x)){displaystyle forall x.R(x,f(x))} 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,
M{displaystyle M} is satisfiable if and only if there exists a model
f{displaystyle f} , which contains an evaluation for
∀x.R(x,f(x)){displaystyle forall x.R(x,f(x))} , such that
∃f∀x.R(x,f(x)){displaystyle exists fforall x.R(x,f(x))} is true for some evaluation of its free variables (none in this case). This may be expressed in second order as
∀x∃y.R(x,y){displaystyle forall xexists y.R(x,y)} . By the above equivalence, this is the same as the satisfiability of
.
At the meta-level, first-order satisfiability of a formula
Φ{displaystyle Phi }∃M∃μ . (M,μ⊨Φ){displaystyle exists Mexists mu ~.~(M,mu models Phi )} may be written with a little abuse of notation as
M{displaystyle M} , where
μ{displaystyle mu } is a model,
⊨{displaystyle models } is an evaluation of the free variables, and
Φ{displaystyle Phi } means that
M{displaystyle M} is true in
μ{displaystyle mu } under
Φ{displaystyle Phi } . Since first-order models contain the evaluation of all function symbols, any Skolem function that
∃M{displaystyle exists M} contains is implicitly existentially quantified by
∃f∀x.R(x,f(x)){displaystyle exists fforall x.R(x,f(x))} . 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
∀x.R(x,f(x)){displaystyle forall x.R(x,f(x))} as
∃M{displaystyle exists M} may be completed because functions are implicitly existentially quantified by
in the definition of first-order satisfiability.
Correctness of Skolemization may be shown on the example formula
F1=∀x1…∀xn∃yR(x1,…,xn,y){displaystyle F_{1}=forall x_{1}dots forall x_{n}exists yR(x_{1},dots ,x_{n},y)}M{displaystyle M} as follows. This formula is satisfied by a model
x1,…,xn{displaystyle x_{1},dots ,x_{n}} if and only if, for each possible value for
y{displaystyle y} in the domain of the model, there exists a value for
R(x1,…,xn,y){displaystyle R(x_{1},dots ,x_{n},y)} in the domain of the model that makes
f{displaystyle f} true. By the axiom of choice, there exists a function
y=f(x1,…,xn){displaystyle y=f(x_{1},dots ,x_{n})} such that
F2=∀x1…∀xnR(x1,…,xn,f(x1,…,xn)){displaystyle F_{2}=forall x_{1}dots forall x_{n}R(x_{1},dots ,x_{n},f(x_{1},dots ,x_{n}))} . As a result, the formula
f{displaystyle f} is satisfiable, because it has the model obtained by adding the evaluation of
M{displaystyle M} to
F1{displaystyle F_{1}} . This shows that
F2{displaystyle F_{2}} is satisfiable only if
F2{displaystyle F_{2}} is satisfiable as well. Conversely, if
M′{displaystyle M’} is satisfiable, then there exists a model
f{displaystyle f} that satisfies it; this model includes an evaluation for the function
x1,…,xn{displaystyle x_{1},dots ,x_{n}} such that, for every value of
R(x1,…,xn,f(x1,…,xn)){displaystyle R(x_{1},dots ,x_{n},f(x_{1},dots ,x_{n}))} , the formula
F1{displaystyle F_{1}} holds. As a result,
x1,…,xn{displaystyle x_{1},ldots ,x_{n}} is satisfied by the same model because one may choose, for every value of
y=f(x1,…,xn){displaystyle y=f(x_{1},dots ,x_{n})} , the value
f{displaystyle f} , where
M′{displaystyle M’} is evaluated according to
.
Uses of Skolemization[edit]
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 may be generated. For example, if
∃x.Φ(x,y1,…,yn){displaystyle exists x.Phi (x,y_{1},ldots ,y_{n})}x,y1,…,yn{displaystyle x,y_{1},ldots ,y_{n}} occurs in a tableau, where
Φ(x,y1,…,yn){displaystyle Phi (x,y_{1},ldots ,y_{n})} are the free variables of
Φ(f(y1,…,yn),y1,…,yn){displaystyle Phi (f(y_{1},ldots ,y_{n}),y_{1},ldots ,y_{n})} , then
f{displaystyle f} may 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 may be extended, by adding a suitable evaluation of
, to a model of the new formula.
This form of Skolemization is 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 tableaux 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 may be used is applying the same Skolem function symbol for formulae that are identical up to variable renaming.[2]
Another use is in the resolution method for first-order logic, where formulas are represented as sets of clauses understood to be universally quantified. (For an example see drinker paradox.)
An important result in model theory is the Lowenheim-Skolem theorem, which can be proven via Skolemizing the theory and closing under the resulting Skolem functions.[3]
Skolem theories[edit]
In general, if
T{displaystyle T}x1,…,xn,y{displaystyle x_{1},dots ,x_{n},y} is a theory and for each formula with free variables
F{displaystyle F} there is a function symbol
y{displaystyle y} that is provably a Skolem function for
T{displaystyle T} , then
is called a Skolem theory.[4]
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.
History[edit]
Skolem normal form is named after the late Norwegian mathematician Thoralf Skolem.
Recent Comments