Actions

Skolemization

From Learning Logic for Computer Science

Skolemization is a process for reducing the satisfiability of arbitrary formulas in prenex normal form to the satisfiability of universal formulas. This is, for instance, important when resolution is used to check for satisfiability.

Example A formula of the form $\exists x_0 \varphi$ is satisfiable if, and only if, $\varphi\{x_0 \mapsto c\}$ is satisfiable, when $c$ is a constant symbol not occurring in $\varphi$.

So, in the simplest case, existential quantification can be eliminated by introducing new constants as far is satisfiablity is concerned. It is, however, important to note that the new formulas are not equivalent to the old ones.

Example In the above example, let $\varphi = P(x_0)$. Clearly, $\exists x_0 P(x_0)$ and $P(c)$ are not equivalent.

Satisfiability reductions

Definition Let $\mathcal S$ and $\mathcal S'$ be signatures such that $\mathcal S \subseteq \mathcal S'$. An $\mathcal S$-formula $\varphi$ reduces to an $\mathcal S'$-formula $\varphi'$, denoted $\varphi \leq_S\varphi'$, if the following two properties are satisfied.

  1. For every $\mathcal S$-structure $\mathcal A$ there exists an $\mathcal S'$-expansion $\mathcal A'$ of $\mathcal A$ such that if $\mathcal A, \beta \mymodels \varphi$, then $\mathcal A', \beta \mymodels \varphi'$ for every $A$-assignment $\beta$.
  1. For every $\mathcal S'$-structure $\mathcal A'$ and $A'$-assignment $\beta$, if $\mathcal A',\beta \mymodels \varphi'$, then $\mathcal A,\beta \mymodels \varphi$ for the $\mathcal S$-reduct $\mathcal A$ of $\mathcal A'$.

This relation has several simple properties.

Lemma

  1. For all first-order formulas $\varphi$ and $\varphi'$, if $\varphi \leq_S \varphi'$, then $\varphi$ is satisfiable if, and only if, $\varphi'$ is satisfiable.
  2. The relation $\leq_S$ is reflexive and transitive, that is, it is a preorder.
  3. For all first-order formulas $\varphi$ and $\varphi'$, if $\varphi \leq_S \varphi'$, then $\forall x_i \varphi \leq_S \forall x_i \varphi'$ for all $i \in \mathbf N$.

Proof For the proof of 1., assume $\varphi \leq_S \varphi'$ as in the definition of $\leq_S$. First, assume $\varphi'$ is satsifiable. Then there exists an $\mathcal S'$-structure $\mathcal A'$ and a variable assignment $\beta$ such that $\mathcal A', \beta \mymodels \varphi'$. Then, by the second property, $\mathcal A,\beta \mymodels \varphi$ for the $\mathcal S$-reduct $\mathcal A$ of $\mathcal S'$. So $\mathcal \varphi$ is satisfiable. For the converse, assume $\varphi$ is satisfiable. Then there exists an $\mathcal S$-structure $\mathcal A$ and a variable assignment $\beta$ such that $\mathcal A, \beta \mymodels \varphi$. By the first property of $\leq_S$, there exists a $\mathcal S'$-expansion $\mathcal A'$ from $\mathcal A$ such that $\mathcal A', \beta \models \varphi'$. So $\varphi'$ is satisfiable.

Clearly, $\varphi \leq_S \varphi$ for every formula $\varphi$. So $\leq_S$ is reflexive. For transitivity, assume $\varphi \leq_S \varphi' \leq_S \varphi' '$ with signatures $\mathcal S \subseteq \mathcal S' \subseteq \mathcal S' '$. We need to show $\varphi \leq_S \varphi' '$. Let $\mathcal A$ be an arbitrary $\mathcal S$-structure. Let $\mathcal A'$ be the $\mathcal S'$-expansion of $\mathcal A$ which exists by the first property ($\varphi \leq_S \varphi'$). Let $\mathcal A' '$ be the $\mathcal S' '$-expansion of $\mathcal A'$ which exists by the first property ($\varphi' \leq_S \varphi' '$). For every $A$-assignment $\beta$ we have:

  • if $\mathcal A, \beta \mymodels \varphi$, then $\mathcal A', \beta \mymodels \varphi'$, and
  • if $\mathcal A', \beta \mymodels \varphi'$, then $\mathcal A' ', \beta \mymodels \varphi' '$, so
  • if $\mathcal A, \beta \mymodels \varphi$, then $\mathcal A' ', \beta \mymodels \varphi' '$,

which shows that the first property holds. For the second property, assume $\mathcal A' ',\beta \mymodels \varphi' '$. Then, by the second property and because $\varphi' \leq_S \varphi' '$, we have $\mathcal A', \beta \mymodels \varphi'$, where $\mathcal A'$ is the $\mathcal S'$-reduct of $\mathcal A' '$. Similarly, we have $\mathcal A, \beta \mymodels \varphi$. So the second property also holds true.

For the proof of 3., assume $\varphi \leq_S \varphi'$ and let $i \in \mathbf N$. We want to show $\forall x_i \varphi \leq_S \forall x_i \varphi'$. To this end, let $\mathcal A$ be an arbitrary $\mathcal S$-structure. We need to construct an appropriate $\mathcal S'$-expansion. We know there exists an $\mathcal S'$-expansion $\mathcal A'$ of $\mathcal A$ such that $\mathcal A,\beta \mymodels \varphi$ iff $\mathcal A',\beta \models \varphi'$. This implies: \begin{align} \mathcal A,\beta \mymodels \forall x_i \varphi & \text{ iff } \mathcal A, \beta\left[ \frac{x_i}{a} \right] \models \varphi \quad \text{for every $a \in A$} \\ & \text{ iff } \mathcal A', \beta\left[ \frac{x_i}{a} \right] \models \varphi' \quad \text{for every $a \in A$} \\ & \text{ iff } \mathcal A', \beta \mymodels \forall x_i \varphi' \enspace. \end{align} Further, let $\mathcal A'$ and $\beta$ be such that $\mathcal A',\beta \mymodels \forall x_i \varphi'$. We need to show $\mathcal A, \beta \mymodels \forall x_i \varphi$ for the $\mathcal S$-reduct $\mathcal A$ of $\mathcal A'$. Now, the above chain of implications holds in the opposite direction.

The crucial property is the following.

Lemma Let $\varphi$ be a first-order formula over some signature $\mathcal S$, $i \in \mathbf N$, and $x_{i_0}, \dots, x_{i_{n-1} }$ an enumeration of the elements of $\text{fvars}(\varphi) \setminus \{x_i\}$. Let $\mathcal S'$ be a signature such that $\mathcal S' = \mathcal S \cup \{f/\!/n\}$. Then \begin{align} \exists x_i \varphi \leq_S \varphi\{x_i \mapsto f(x_{i_0}, \dots, x_{i_{n-1} })\} \enspace, \end{align} provided there is no name clash for the substitution in $\varphi$.

Proof For the first property, assume $\mathcal A$ is an $\mathcal S$-structure. We define an $\mathcal S'$-expansion $\mathcal A'$ of $\mathcal A$. For every variable assignment $\beta$, if $\mathcal A,\beta \mymodels \exists x_i \varphi$, then there is some $a \in A$ such that $\mathcal A, \beta\left[ \frac{x_i}{a}\right] \models \varphi$. We set $f^{\mathcal A'}(\beta(x_{i_0}), \dots, \beta(x_{i_{n-1} })) = a$. Then $\mathcal A', \beta \mymodels \varphi \{x_i \mapsto f(x_{i_0}, \dots, x_{i_{n-1} })\}$ by the substitution lemma.

For the second property, assume $\mathcal A', \beta \mymodels \varphi \{x_i \mapsto f(x_{i_0}, \dots, x_{i_{n-1} })\}$ and let $\mathcal A$ be the $\mathcal S$-reduct of $\mathcal A'$. We then have, again by the substitution lemma, $\mathcal A, \beta\left[\frac{x_i}{f^{\mathcal A'}(\beta(x_{i_0}), \dots, \beta(x_{i_{n-1} }))}\right] \models \varphi$, so $\mathcal A,\beta \mymodels \exists x_i \varphi$.

Skolemization

Given an arbitrary formula $\varphi$ in prenex normal form, that is, $\varphi = B \psi$ for a quantifier prefix $B$ and a matrix $\psi$, there is a straightforward way of turning this formula into a universal formula $\varphi'$ such that $\varphi \leq_S \varphi'$: The procedure starts out from $\psi$ and adds the quantifications from $B$ one at a time. Universal quantifications are added just as they are. Existential quantification are replaced by substitutions and augmenting the signature as in the above lemma, possibly after a renaming of the quantified variables to avoid name clashes.

Example The formula $\forall x_0 \exists x_1 (E(x_0, x_1) \wedge \neg E(x_0, x_1))$ is a formula, but not a universal one. We have $\exists x_1 (E(x_0, x_1) \wedge \neg E(x_0, x_1)) \leq_S (E(x_0, f(x_0)) \wedge \neg E(x_0, f(x_0)))$ by the second lemma. We then have $\forall x_0 \exists x_1 (E(x_0, x_1) \wedge \neg E(x_0, x_1)) \leq_S \forall x_0 (E(x_0, f(x_0)) \wedge \neg E(x_0, f(x_0)))$ by the first lemma. And, overall, we have that the given formula is satisfiable if, and only if, the last formula is satisfiable and (!) universal.