Version without JavaScript, read-only: workshops, quizzes and running code are not available here. Full version · Catalogue · Sign in
Lecture notes · chapter 9
Prenex normal form and Skolemisation
Moving all the quantifiers to the front, replacing the “there exists” by functions, and arriving at clauses, ready for resolution.
Where we are going
The resolution of chapter 5 works on clauses. To extend it to first order (chapter 10), we must bring every formula to a set of clauses. Three steps:
- prenex normal form: all the quantifiers at the front;
- Skolemisation: no more $\exists$;
- clausal form: the quantifier-free part in CNF, the $\forall$ left implicit.
The first keeps the meaning of the formula. The second does not, but keeps what matters for refutation: satisfiability.
Prenex normal form
Definition
A formula is in prenex normal form if it can be written $Q_1 x_1\, Q_2 x_2 \ldots Q_n x_n\, M$, where each $Q_i$ is $\forall$ or $\exists$, and where $M$, the matrix, contains no quantifier.
Example: $\forall x\, \exists y\, (P(x) \to R(x, y))$ is prenex; $\forall x\, P(x) \to \exists y\, Q(y)$ is not.
The rules for moving a quantifier out
In addition to the equivalences of chapter 8, we use these, provided that $x$ is not free in $B$:
| Formula | Equivalent to |
|---|---|
| $\forall x\, A \land B$ | $\forall x\, (A \land B)$ |
| $\exists x\, A \land B$ | $\exists x\, (A \land B)$ |
| $\forall x\, A \lor B$ | $\forall x\, (A \lor B)$ |
| $\exists x\, A \lor B$ | $\exists x\, (A \lor B)$ |
| $B \to \forall x\, A$ | $\forall x\, (B \to A)$ |
| $B \to \exists x\, A$ | $\exists x\, (B \to A)$ |
| $\forall x\, A \to B$ | $\exists x\, (A \to B)$ |
| $\exists x\, A \to B$ | $\forall x\, (A \to B)$ |
The last two rows are surprising: a quantifier that moves out of the left side of an implication changes its nature. This is because $A \to B \equiv \lnot A \lor B$, and negation swaps $\forall$ and $\exists$.
The method
- Eliminate $\leftrightarrow$ (and, if you wish, $\to$).
- Rename the bound variables so that they are all different from one another, and different from the free variables. This is what guarantees the condition “$x$ is not free in $B$”.
- Move the quantifiers out one by one with the rules, from the inside out.
The prenex form is not unique: when two quantifiers move out of the two sides of a $\land$, they can be moved out in either order. All the results are equivalent.
Skolemisation
The idea
In $\forall x\, \exists y\, R(x, y)$, the $y$ depends on $x$: for each $x$, there is a $y$. We can give a name to this choice: a function $f$ which maps each $x$ to such a $y$. The formula becomes $\forall x\, R(x, f(x))$. The new symbol $f$ is called a Skolem function (Thoralf Skolem, 1920).
The method
On a prenex formula, we handle the $\exists$ from left to right. For each $\exists y$:
- we delete it;
- we replace $y$, in the matrix, by $f(x_1, \ldots, x_k)$, where $f$ is a fresh symbol, and where $x_1, \ldots, x_k$ are the variables of the $\forall$ placed before this $\exists$;
- if there is no $\forall$ before it, $f$ has no argument: it is a fresh constant.
What Skolemisation preserves
The Skolemised formula is not equivalent to the original one: $P(a)$ states something about the object $a$, $\exists x\, P(x)$ does not. But they are equisatisfiable: one has a model if and only if the other has one. That is all resolution needs, since it precisely seeks to show that a set has no model.
Clausal form
After Skolemisation, only $\forall$ remain at the front. We put the matrix in CNF (chapter 3), then:
- we leave the $\forall$ implicit: every variable of a clause is universally quantified;
- we separate the clauses;
- we rename the variables so that two different clauses do not share any. This is allowed, since $\forall x\, (A \land B) \equiv \forall x\, A \land \forall y\, B[x := y]$.