Skolemization

Skolemization is the process of eliminating existential quantifiers from a formula in predicate logic viapredicate substitution.

Definition §

Skolemization ^definition

A formula in predicate logic of the form $P=\forall x_1\forall x_2\dots \forall x_n\exists yQ$ where $Q$ is a predicate and $x_i,y$ are variables can be Skolemized by a predicate substitution:

$$\theta =\{y\mapsto f(x_1,x_2,\dots x_n)\}$$

• $f$ is a Skolem function, and must be a fresh function symbol (i.e. a function not already in $P$)
• $f(x_1\dots x_n)$ is known as a Skolem term
• $P[\theta ]$ results in the $\exists y$ being eliminated from the formula.

If the $\exists y$ is in universal/global scope (i.e. outermost), then the substitution:

$$\theta =\{y\mapsto c\}$$

where $c$ is a Skolem constant can be used instead

Skolemization does not preserve semantic properties!

Because Skolemization uses predicate substitution, which only preserves equisatisfiability, the Skolemized form of a formula is not logically equivalent to the original formula. However, if the original formula is satisfiable, so is its Skolem form.

Explanation §

We can use substitution to eliminate the existential quantifier ($\exists$) when it is the ‘outermost’ quantifier. Let $F=\exists x\forall yP(x,y)$:

• $F$ is a predicate
• $x,y$ are variables
• $a$ is a constant

We can ‘fix’ the value of the $x$ in $F$. Let us call the new formula $G$.

$$\exists x\forall yP(x,y)\stackrel{x\mapsto a}{\to }\forall yP(a,y)$$

$$F\stackrel{x\mapsto a}{\to }G$$

This elimination by substitution preserves satisfiability:

Take the formula:

$$\forall y\exists xP(x,y)$$

We can’t do the eliminating existential quantifiers method, because the $\exists$ is not in the outermost level. Essentially we can’t ‘fix’ a single value of $x$ because we need different values of $x$ for each value of $y$ (since we are ranging over $y$). But if we have some way of representing $x$ in terms of $y$. Like… a function!

Let’s substitute $x\mapsto f(y)$

$$\forall yP(f(y),y)$$

This method is known as Skolemization.