Questions: Substitution and Unification

Question 1

You try to substitute y for x in the formula ∃y (x = y), obtaining ∃y (y = y). What went wrong?

• A. Nothing — substitution always replaces all variable occurrences and ∃y (y = y) is correct
• B. Variable capture: the free y being substituted fell under the ∃y quantifier, changing the formula's meaning from 'there exists something equal to x' to 'something equals itself'
• C. Substitution is not allowed inside quantifier scopes
• D. The error is that x is bound in ∃y (x = y), so substitution cannot apply

Answer: (B)

This is the canonical variable capture bug. In ∃y (x = y), x is free (not under any quantifier for x) — so substitution of y for x is allowed. But the y being substituted happens to be the same name as the bound variable ∃y. Naively replacing x with y gives ∃y (y = y), which means 'something equals itself' — a tautology true of everything. The original formula means 'there is something equal to x' — a different, non-trivial claim. The fix is alpha-conversion: rename the bound variable first (∃z (x = z)), then substitute safely to get ∃z (y = z).

Question 2

What is the 'occurs check' in Robinson's unification algorithm, and why does failing to perform it cause problems?

• A. It checks whether a term has already appeared in a previous unification step, to avoid redundant work
• B. It prevents a variable x from being unified with a term t that contains x, which would require an infinite term to satisfy x = t
• C. It verifies that function symbols match before recursing on subterms
• D. It checks that both terms have the same number of arguments before attempting unification

Answer: (B)

The occurs check prevents extending the unifier with x ↦ t when x appears inside t. If you allowed x ↦ f(x), you'd need x to equal f(f(f(…))) — an infinite term. Standard first-order logic requires finite terms, so this unification must fail. Skipping the occurs check (as Prolog does for performance reasons) can lead to infinite loops or unsound inferences when cyclic bindings are created. The occurs check is the safeguard that keeps unification within well-formed finite terms.

Question 3

Substitution φ[t/x] replaces most occurrences of the variable x in formula φ — including those that appear under quantifiers like ∀x or ∃x.

• T. True
• F. False

Answer: False

Substitution replaces only FREE occurrences of x — those not bound by a quantifier. An occurrence of x under ∀x or ∃x is a bound occurrence and refers to a different, locally scoped variable that happens to share the name x. Substituting into a bound occurrence would change the quantifier's scope incorrectly. The notation φ[t/x] is defined to be capture-avoiding and to leave bound occurrences untouched. This is emphasized in the Common Misconceptions: 'Substitution only replaces free occurrences — bound occurrences of the same variable name are untouched.'

Question 4

The most general unifier (MGU) is the most specific substitution possible — it assigns concrete values to most variable to make the two terms identical.

• T. True
• F. False

Answer: False

The MGU is the LEAST committal unifier, not the most specific. It makes only the minimum variable assignments required to achieve syntactic identity, leaving all other variables free. Any other unifier for the same pair of terms can be obtained by composing the MGU with a further substitution. Using a more specific unifier than the MGU forecloses future flexibility — in resolution theorem proving, this means committing to variable values prematurely and potentially blocking valid inferences. The 'most general' means least constrained, not most detailed.

Question 5

Why is the most general unifier preferred over other unifiers in resolution theorem proving and logic programming?

Model answer: The MGU is preferred because it makes the minimum commitments necessary to unify two terms, leaving all other variables free to be instantiated later. In resolution, each inference step unifies complementary literals and applies the resulting substitution to the entire clause — a substitution that assigns values to variables affects all future reasoning steps. Using a more specific unifier than necessary prematurely constrains variables that might need different values in subsequent steps, potentially blocking valid proofs. The MGU preserves maximum flexibility: any other unifier for the same terms is a special case of the MGU under further substitution.

The point is that logical inference is non-deterministic — the correct instantiation of a variable often isn't determined until several steps later. Committing to x = a when x = f(b) might be needed downstream is an irreversible error. The MGU is the uniquely correct choice because it defers all commitments except those forced by the current unification task. This is why Robinson's algorithm explicitly computes the MGU rather than any unifier.