Clause form & Skolemization (bridge to resolution)

◈ 4 cards

Convert a sentence toward clause/CNF form and apply Skolemization (∀X∃Y mother(X,Y) ⇒ ∀X mother(X, m(X))); know the Skolem-constant vs Skolem-function rule. Light touch — sets up Module 9 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:

Eliminate $\to$ and $\equiv$ using $P \to Q \equiv \neg P \lor Q$ .
Push negations inward with De Morgan and the quantifier-negation rules ( $\neg\forall \equiv \exists\neg$ ), until every $\neg$ sits on an atomic sentence.
Standardise variables apart so no two quantifiers share a variable name.
Skolemize — remove every existential quantifier (below).
Drop the universal quantifiers (all remaining variables are implicitly universal) and distribute $\lor$ over $\land$ 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 p r es i d e n t (X)$ becomes $p r es i d e n t (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 m o t h er (X, Y) ⟹ \forall X m o t h er (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 m o t h er (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 m o t h er (X, m (X))$ . Contrast "there exists a perfect being", $\exists X p er f ec t (X)$ , with no universal in scope: the existential becomes a Skolem constant, $p er f ec t (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.

The pipeline is mechanical and order matters: implications must go before negations can be pushed in, and variables must be standardised apart before Skolemization, or two unrelated existentials collapse onto one Skolem term. Only the highlighted step needs judgement — <strong>constant when no ∀ surrounds the ∃, function of the surrounding ∀-variables when one does</strong>.