Questions: Quantifier Instantiation Rules in First-Order Proof Systems

Question 1

From the premise ∀x ∀y (x + y = y + x), which is a valid application of Universal Instantiation?

• A. ∃x ∃y (x + y = y + x) — existential generalization is needed since the statement covers everything
• B. a + b = b + a — substituting constants a and b for x and y respectively
• C. x + y = y + x — simply removing the quantifier symbols but keeping the variables
• D. ∀y (0 + y = y + 0) — partially instantiating x with 0 while keeping the remaining universal

Answer: (B)

Universal Instantiation (∀-Elim) licenses substituting any term for the bound variable. Substituting x←a and y←b gives 'a + b = b + a' — a valid specific instance. Option A applies the wrong rule (EG goes from specific to existential, not from universal to existential). Option C leaves variables free and unquantified, which is syntactically problematic. Option D is actually valid (partial instantiation), but option B is the clearest correct application; in a formal proof we'd apply UI once per quantifier.

Question 2

To prove ∃x (x > 5) using Existential Generalization, what must you establish first?

• A. Write ∃x (x > 5) directly as a logical axiom, since the claim is obviously true
• B. First prove a specific instance — e.g., derive (7 > 5) — then apply EG to conclude ∃x (x > 5)
• C. Apply UI to ∀x (x > 5) to obtain the existential claim
• D. Assume ¬∃x (x > 5) and derive a contradiction

Answer: (B)

Existential Generalization (∃-Intro/EG) works from specific to general: from φ[t/x] (a specific witness), derive ∃x φ(x). You prove '7 > 5', then generalize over the witness 7 to get ∃x (x > 5). Option A skips the proof step entirely. Option C misapplies UI — UI goes from universal down to specific, not to existential. Option D is a valid indirect proof strategy but is not EG.

Question 3

Universal Instantiation allows substituting a complex term — like f(a) or (b + 1) — for a universally quantified variable, not only simple constants.

• T. True
• F. False

Answer: True

UI states: from ∀x φ(x), derive φ[t/x] for any term t. The term t can be any constant, any variable, or any complex expression built from function symbols — as long as t is free for x in φ (no variable in t becomes accidentally bound inside φ). From ∀x (x + 0 = x) you can derive f(a) + 0 = f(a) by substituting t = f(a). This flexibility is what makes universals so powerful: one formula licenses infinitely many instantiations.

Question 4

To prove ∀x φ(x) in natural deduction, it is sufficient to verify that φ holds for several specific constants.

• T. True
• F. False

Answer: False

Checking specific cases does not constitute a formal proof of a universal. ∀-Introduction (∀-Intro) requires deriving φ(c) for a completely *arbitrary* constant c — one introduced with no assumptions about it, so nothing specific about c made the proof work. Verifying φ(a), φ(b), and φ(0) only establishes φ for three particular objects. This is why finite examples can't establish universal mathematical facts in a proof system — you need the argument to work for an unspecified, unconstrained c.

Question 5

What is variable capture in Universal Instantiation, and why is it a problem? Give a brief example.

Model answer: Variable capture occurs when substituting term t for x in φ causes a free variable in t to fall inside the scope of a quantifier already in φ, changing the formula's meaning. Example: from ∀x ∃y (x ≠ y), naively instantiating x←y gives ∃y (y ≠ y), which is false — the free y was captured by the ∃y quantifier, producing an unsatisfiable formula. The correct fix is alpha-renaming: first rewrite the premise as ∀x ∃z (x ≠ z), then substitute x←y to get ∃z (y ≠ z), which is both meaningful and true. Variable capture is why UI includes the 'free for x in φ' side condition.

Variable capture is the principal technical hazard in quantifier reasoning. Systematically alpha-renaming bound variables to fresh names before any substitution eliminates all capture risks and is standard practice in both formal proof assistants and careful hand proofs.