Questions: Skolemization and Equisatisfiability

Question 1

A logician Skolemizes the formula ∀x ∃y P(x, y) to obtain ∀x P(x, f(x)). What is the correct relationship between the original and the Skolemized formula?

• A. They are logically equivalent — every model of one is a model of the other
• B. They are equisatisfiable — a model for one exists if and only if a model for the other exists — but the Skolemized version is logically stronger
• C. The Skolemized version implies the original, but not vice versa — Skolemization weakens the formula
• D. They are neither equivalent nor equisatisfiable — Skolemization changes the meaning of the formula

Answer: (B)

Equisatisfiability, not logical equivalence, is the correct relationship. Any model M of ∀x ∃y P(x,y) can be extended to a model of ∀x P(x,f(x)) by interpreting f as a choice function that picks a witness y for each x. Conversely, any model of ∀x P(x,f(x)) satisfies ∀x ∃y P(x,y) by existential introduction (let y = f(x)). So they are satisfiable in the same circumstances. However, ∀x P(x,f(x)) is logically stronger: it requires a *uniform* function f witnessing all instances simultaneously, while ∀x ∃y P(x,y) only requires that for each x some witness exists, possibly varying with the model. There are models of the original that cannot interpret f in the required way for the Skolemized version.

Question 2

When Skolemizing ∃y ∀x P(x, y) — where the existential quantifier is outermost — the correct Skolemized form is:

• A. ∀x P(x, f(x)), with a Skolem function f taking x as argument
• B. ∀x P(x, c), with a Skolem constant c (a 0-ary function symbol)
• C. P(x, y) with both quantifiers dropped and variables left free
• D. ∀x ∃y P(x, y), since the existential is moved inward

Answer: (B)

The rule for Skolemization is: when eliminating ∃y, introduce a fresh function symbol whose arguments are all universally quantified variables in scope *before* y in the prenex prefix. When ∃y is the outermost quantifier, there are no preceding ∀ quantifiers, so the Skolem term is a constant c (a 0-ary function) — the witness doesn't depend on anything. The formula becomes ∀x P(x, c). If the formula were instead ∀x ∃y P(x,y), then y's witness could depend on x, so we'd use f(x). The key is tracking the ordering of quantifiers in the prefix.

Question 3

Skolemization preserves logical equivalence: a formula φ and its Skolemization φ_S are true in exactly the same models.

• T. True
• F. False

Answer: False

This is the most important misconception about Skolemization. Skolemization preserves *satisfiability* (they have models in the same circumstances), not logical equivalence (they are not true in exactly the same models). The Skolemized formula φ_S is logically stronger: it asserts the existence of a specific function symbol (Skolem function) that uniformly witnesses all instances of the existential quantifier. In models where witnesses exist but no uniform function works, φ is true but φ_S is false. This is why Skolemization cannot be reversed and why it is called equisatisfiability, not equivalence.

Question 4

Equisatisfiability is exactly the right property for automated theorem proving because resolution works on clause sets that require all existential quantifiers to be eliminated first.

• T. True
• F. False

Answer: True

Resolution works on Horn clauses and general clause sets — quantifier-free formulas where all variables are implicitly universally quantified. To apply resolution to a first-order formula with existential quantifiers, you must first convert to prenex normal form and then Skolemize to eliminate the existentials. The result is a universally quantified formula that, after dropping the universal quantifiers (since variables are implicitly universal in clause form), can be converted to CNF clauses. Equisatisfiability is sufficient: if the original formula is unsatisfiable, so is its Skolemization, and resolution can detect this by deriving the empty clause. Logical equivalence is not needed and in fact cannot be preserved by the quantifier-elimination step.

Question 5

Why does Skolemization preserve satisfiability but not logical equivalence, and why is satisfiability-preservation sufficient for automated theorem proving via resolution?

Model answer: Satisfiability is preserved because: if φ has a model, that model's existential witnesses can be used to define Skolem functions, extending the model to satisfy φ_S; conversely, any model of φ_S satisfies φ by existential introduction. Logical equivalence fails because φ_S is stronger: it commits to a specific choice function for all instances, while φ only requires that some witness exists in each model independently. For automated theorem proving, satisfiability-preservation suffices because resolution proves unsatisfiability: to prove a theorem T, you negate it, Skolemize, convert to clauses, and run resolution. If the original negation was unsatisfiable, the Skolemized version is too (by equisatisfiability), and resolution will find a refutation. No stronger property is needed.

The critical point is what resolution is *doing*: it is searching for a refutation (proof that a set of clauses is unsatisfiable). For this purpose, you only need to know that satisfiability is the same before and after Skolemization. If you needed to reconstruct models or reason about truth in specific interpretations, logical equivalence would matter. But since refutation only cares about whether a model exists at all, equisatisfiability is precisely the right property — no stronger, no weaker.