Clause form & Skolemization (bridge to resolution)

Why a normal form

The resolution inference rule (Module 9) is sound *and* complete, but it only works on sentences in a uniform shape called clause form — a conjunction of clauses, each clause a disjunction of literals (a literal is an atomic sentence or its negation). Converting an arbitrary predicate-calculus sentence to clause form is mechanical. You do not need all nine steps in detail yet; you need the idea and the one step that is genuinely subtle: Skolemization.

The conversion, sketched

Using the laws from Lesson 2 plus the quantifier rules from Lesson 4, the procedure broadly is:

1. Eliminate $\to$ and $\equiv$ using $P \to Q \equiv \neg P \vee Q$.
2. Push negations inward with De Morgan and the quantifier-negation rules ($\neg\forall \equiv \exists\neg$), until every $\neg$ sits on an atomic sentence.
3. Standardise variables apart so no two quantifiers share a variable name.
4. Skolemize — remove every existential quantifier (below).
5. Drop the universal quantifiers (all remaining variables are implicitly universal) and distribute $\vee$ over $\wedge$ to reach conjunctive normal form, then split into clauses.

Skolemization: removing $\exists$

An existential says "there *is* some object". We name that object instead of quantifying it. Two cases:

- No universal in scope → replace the existential variable with a brand-new Skolem constant. $\exists X\,president(X)$ becomes $president(c_1)$ where $c_1$ is a fresh constant naming "the president that exists". - Inside one or more universals → replace it with a Skolem function of those universal variables, because *which* object exists may depend on them. The classic example:

$$\forall X\,\exists Y\,mother(X, Y) \;\Longrightarrow\; \forall X\,mother(X, m(X))$$

"Everyone has a mother" — the *particular* mother depends on the person $X$, so the existential $Y$ becomes the Skolem function $m(X)$ ("the mother of $X$"). A Skolem function is not a new predicate; it is a *term*-level construct capturing the dependency of the existential witness on the surrounding universals.

Worked example

Take "every person has a mother": $\forall X\,\exists Y\,mother(X, Y)$. There is a universal $X$ in scope around the existential $Y$, so $Y$ is replaced by a Skolem function $m(X)$, giving $\forall X\,mother(X, m(X))$. Contrast "there exists a perfect being", $\exists X\,perfect(X)$, with no universal in scope: the existential becomes a Skolem constant, $perfect(c_1)$. The rule of thumb: constant when no ∀ surrounds it, function of the surrounding ∀-variables when one does. Skolemization is required *before* unification (Lesson 6), because the unify algorithm assumes every variable is universally quantified.