Skolem normal form: Difference between revisions

Content deleted Content added

Inline

Revision as of 00:06, 2 February 2006

A formula of first-order logic is in Skolem normal form if its prenex normal form has only universal quantifiers. A formula can be Skolemized, that is have its existential quantifiers eliminated to produce an equisatisfiable formula to the original. Skolemization is an application of the (second-order) equivalence

\forall x\exists yR(x,y)\Leftrightarrow \exists f\forall xR(x,f(x))

The essence of Skolemization is the observation that if a formula in the form

\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)

is satisfiable in some model, then there must be some point in the model for every

x_{1},\dots ,x_{n}

which makes

R(x_{1},\dots ,x_{n},y)

true, and there must exist some function

y=f(x_{1},\dots ,x_{n})

which makes the formula

\forall x_{1}\dots \forall x_{n}M(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))

The function f is called a Skolem function.

This mathematics-related article is a stub. You can help Wikipedia by expanding it.

External links

Skolemization on PlanetMath.org

@@ Line 1: / Line 1: @@
 A [[formula]] of [[first-order logic]] is in '''Skolem normal form''' if its [[prenex normal form]] has only universal quantifiers.  A formula can be '''Skolemized''', that is have its existential quantifiers eliminated to produce an [[satisfiable|equisatisfiable]] formula to the original. Skolemization is an application of the ([[second-order logic|second-order]]) equivalence
-:<math>\forall x \exists y M(x,y) \Leftrightarrow \exists f \forall x M(x,f(x))</math>
+:<math>\forall x \exists y R(x,y) \Leftrightarrow \exists f \forall x R(x,f(x))</math>
 The essence of Skolemization is the observation that if a formula in the form
-:<math>\forall x_1 \dots \forall x_n \exists y M(x_1,\dots,x_n,y)</math>
+:<math>\forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)</math>
 is satisfiable in some [[model (abstract)|model]], then there must be some point in the model for every
@@ Line 13: / Line 13: @@
 which makes
-:<math>M(x_1,\dots,x_n,y)</math>
+:<math>R(x_1,\dots,x_n,y)</math>
 true, and there must exist some function