Questions: Substitution and Instantiation in Predicate Logic

Question 1

We want to substitute y for x in the formula ∃y (y > x), writing φ[y/x]. Naive substitution produces ∃y (y > y). What went wrong?

• A. Only constants may be substituted for variables — substituting a variable for a variable is always invalid
• B. The free variable y in the substituted term was captured by the quantifier ∃y in the formula, producing a formula with a completely different meaning
• C. Universal instantiation applies only to ∀, so this substitution requires a different rule
• D. The substitution is valid — ∃y (y > y) is logically equivalent to ∃y (y > x)

Answer: (B)

The free variable y we tried to introduce got 'captured' by the existing quantifier ∃y, which now binds it. The original formula ∃y (y > x) means 'something is larger than x' — true for most x. After naive substitution, ∃y (y > y) means 'something is larger than itself' — false in any standard order. The meaning changed entirely. The fix is alpha-renaming: first rename the bound variable to z, giving ∃z (z > x), then substitute to get ∃z (z > y), which correctly means 'something is larger than y.'

Question 2

From ∀x P(x), which of the following instantiations are valid under universal instantiation?

• A. Only P(a) for a specific constant a — universal instantiation works only for constants
• B. Only P(x) — reinstantiating the same variable is the safe choice
• C. P(a) or P(b) for constants, but not P(f(a,b)) for complex terms
• D. P(t) for any term t in the domain — constants, variables, or complex function expressions

Answer: (D)

Universal instantiation says: from ∀x φ(x), derive φ(t) for ANY term t — a numeral, a variable, a function applied to other terms, anything in the domain. From ∀x (x + 0 = x) you can derive 5 + 0 = 5, or y + 0 = y, or (a + b) + 0 = (a + b). The power of universal statements is precisely that they license instantiation with arbitrarily complex terms. The only constraint is capture-avoidance: if t contains free variables, make sure those variables are not bound in φ.

Question 3

Capture-avoiding substitution is only necessary when the substituted term is a variable; substituting a constant never causes variable capture.

• T. True
• F. False

Answer: True

Variable capture occurs when a free variable in the substituted term t gets bound by a quantifier in the target formula. Constants have no free variables — there is nothing to capture. If t = 5 or t = a (a constant), substituting it for x in any formula is always safe; no quantifier can bind a constant. Capture is exclusively a problem when t contains free variables that could be 'swallowed' by a quantifier in the formula.

Question 4

The formula φ[t/x] usually has the same logical meaning as φ, just with t appearing where x was.

• T. True
• F. False

Answer: False

This is only true for capture-avoiding substitution. Naive substitution can radically change meaning through variable capture, as in ∃y (y > x)[y/x] = ∃y (y > y), which changes 'something is greater than x' (often true) to 'something is greater than itself' (always false). Capture-avoiding substitution — with alpha-renaming when needed — preserves meaning. The claim that substitution always preserves meaning confuses a correct procedure with its naive (and incorrect) version.

Question 5

What is 'variable capture' in predicate logic substitution, and how does capture-avoiding substitution prevent it? Use an example.

Model answer: Variable capture occurs when a free variable in the term being substituted accidentally becomes bound by a quantifier in the target formula, changing the formula's meaning. Example: substituting y for x in ∃y (y > x) naively gives ∃y (y > y) — the y we introduced is now bound by ∃y. Capture-avoiding substitution prevents this by alpha-renaming the offending bound variable before substituting: first rename bound y to z, giving ∃z (z > x), then substitute to get ∃z (z > y), which preserves the intended meaning.

The key insight is that bound variable names are arbitrary — ∃y (y > x) and ∃z (z > x) are logically identical (alpha-equivalent). Alpha-renaming exploits this: we can always rename a bound variable to one that does not appear free in the term we are substituting, making the substitution safe. This is not just a theoretical nicety — proof assistants, compilers, and logic programming systems must implement capture-avoiding substitution correctly or risk silently producing wrong results.