Questions: Conversion to Clausal Form

Question 1

After applying the full clausal-form conversion pipeline to ∀x (P(x) → ∃y Q(x,y)), what is the result?

• A. A logically equivalent formula ∀x (¬P(x) ∨ Q(x, f(x)))
• B. An equisatisfiable clause {¬P(x), Q(x, f(x))} with f a Skolem function
• C. The formula remains unchanged because it is already in prenex form
• D. Two clauses: {¬P(x)} and {Q(x, f(x))}

Answer: (B)

The implication expands to ∀x (¬P(x) ∨ ∃y Q(x,y)), PNF pulls the quantifier out to ∀x ∃y (¬P(x) ∨ Q(x,y)), Skolemization replaces y with f(x) giving ∀x (¬P(x) ∨ Q(x,f(x))), and dropping the universal prefix yields the single clause {¬P(x), Q(x,f(x))}. Option A says 'logically equivalent' — this is the key error. Skolemization preserves satisfiability, not logical equivalence; the Skolemized formula has a richer signature (f is a new symbol) and is not equivalent to the original.

Question 2

A student claims the clausal form of a first-order formula is 'just CNF with quantifiers added back.' What is wrong with this claim?

• A. Nothing — clausal form is exactly quantified CNF
• B. Clausal form requires removing existential quantifiers via Skolemization, so no quantifiers appear in the final clause set
• C. Clausal form only applies to propositional logic, not first-order logic
• D. In clausal form, universal quantifiers are moved to the inside of each clause

Answer: (B)

The student's claim misses the Skolemization step. Clausal form eliminates all existential quantifiers by replacing them with Skolem functions. The resulting clause set has only universally quantified variables, and by convention those universal quantifiers are dropped — variables are understood to be universally quantified. This is not 'CNF with quantifiers added back'; it is a quantifier-free clause set that is equisatisfiable with, but not logically equivalent to, the original.

Question 3

A first-order formula and its clausal form are logically equivalent.

• T. True
• F. False

Answer: False

Clausal form conversion involves Skolemization, which preserves satisfiability but not logical equivalence. The Skolemized formula introduces new function symbols not in the original vocabulary, and the two formulas make claims about different signatures. They are equisatisfiable — one has a model iff the other does — but they are not equivalent. For example, ∃y Q(y) and Q(f) (where f is a Skolem constant) have different models in general.

Question 4

After Skolemization of a prenex normal form formula, all remaining variables in the clause set are implicitly universally quantified.

• T. True
• F. False

Answer: True

Skolemization replaces each existential quantifier ∃x with a Skolem function applied to all enclosing universal variables. Once every existential is eliminated, only universal quantifiers remain. By the convention of clausal form, these universal quantifiers are then dropped: in each clause, any variable symbol is understood to be universally quantified over all values in the domain. This is what makes the clause set directly usable by resolution-based theorem provers.

Question 5

Why does Skolemization produce a formula that is equisatisfiable with the original rather than logically equivalent to it? What is lost in the transformation?

Model answer: Skolemization replaces existential quantifiers with Skolem functions, which 'choose' witnesses in a vocabulary-dependent way. The Skolemized formula is satisfiable in exactly the same models as the original — if the original is satisfiable, a Skolem model can be constructed; if not, neither is the Skolemized version. But logical equivalence requires the same truth value in all interpretations over the same signature, and the Skolemized formula has extra function symbols the original lacks. It commits to a specific witnessing function, while the original merely asserts existence.

The distinction matters for theorem proving: resolution refutation only requires equisatisfiability (to prove unsatisfiability, we need the clause set to be unsatisfiable iff the original is). Skolemization enables this — it turns existential witnesses into explicit terms manipulable by unification, at the cost of logical equivalence.