Questions: Variable Substitution and Capture-Avoidance in First-Order Logic

Question 1

In the formula ∃y P(x, y), we attempt to substitute y for x. The naive result ∃y P(y, y) is problematic because:

• A. The formula now has no free variables, which is always a logical error
• B. The variable y in the substituted term was captured by the quantifier ∃y, changing the meaning from 'P holds between external y and some z' to 'P holds between some element and itself'
• C. First-order logic does not allow the same variable to appear twice in one formula
• D. The existential quantifier must be removed before any substitution can occur

Answer: (B)

The original formula ∃y P(x, y) says 'there exists some y such that P holds between x and y.' Substituting y for x should give 'there exists some y such that P holds between [the external y we substituted] and y.' But naively writing ∃y P(y, y) instead says 'there exists some y such that P holds between y and itself' — a completely different claim. The external y we intended to substitute has been captured by the quantifier ∃y and treated as a locally bound variable. The free y in the substituted term and the bound y of the quantifier have been conflated, corrupting the meaning.

Question 2

How do you safely perform the substitution [y/x] (substitute y for x) in the formula ∃y P(x, y) to avoid variable capture?

• A. Replace only the first occurrence of x, leaving subsequent occurrences unchanged
• B. Rename the bound variable: replace ∃y P(x,y) with the α-equivalent ∃z P(x,z), then substitute to get ∃z P(y,z)
• C. Apply the substitution conditionally: only substitute x occurrences that appear before the ∃y quantifier
• D. Wrap the substituted term in parentheses: ∃y P((y), y)

Answer: (B)

The correct fix is α-renaming: before substituting, rename the bound variable ∃y to a fresh variable ∃z, giving the logically equivalent ∃z P(x, z). Since z does not appear free in the term y we are substituting, there is no capture risk. Substituting y for x now safely gives ∃z P(y, z), which correctly says 'there exists some z such that P holds between y and z' — exactly the intended meaning. α-renaming is always safe because ∀x φ(x) and ∀z φ(z) are logically identical (α-equivalent): the choice of bound variable name is arbitrary.

Question 3

Renaming a bound variable in a formula — for example, changing ∀x P(x) to ∀z P(z) — preserves the logical meaning of the formula.

• T. True
• F. False

Answer: True

This is the principle of α-equivalence: two formulas that differ only in the names of their bound variables express exactly the same logical content. ∀x P(x) says 'for everything, P holds of it'; ∀z P(z) says exactly the same thing. The bound variable name is a local placeholder — it has no meaning outside its quantifier's scope. α-renaming is the standard tool for avoiding variable capture: by choosing fresh variable names for bound variables, we ensure that free variables in substituted terms cannot be confused with locally bound variables.

Question 4

Substituting a ground term (a term with no variables, such as a constant c) for a free variable generally risks variable capture.

• T. True
• F. False

Answer: False

Variable capture only occurs when the term being substituted contains free variables that could be captured by quantifiers in the formula. A ground term contains no variables at all — it cannot be captured by anything, because there is nothing to capture. Substituting the constant c for x in ∃y P(x, y) safely gives ∃y P(c, y), with no capture possible. This is precisely why proof procedures in logic — such as Henkin constructions and tableaux proofs — routinely use fresh constants (witness constants) as substitution terms: ground terms are automatically capture-free.

Question 5

What is variable capture, and why does capture-avoidance matter for the correctness of logical proof rules like universal instantiation?

Model answer: Variable capture occurs when a free variable in a substituted term becomes bound by a quantifier in the formula it is substituted into, changing the formula's meaning. For example, naively substituting y for x in ∃y P(x,y) gives ∃y P(y,y), where y's meaning has been corrupted from an external value to a locally bound variable. Universal instantiation — concluding φ(t) from ∀x φ(x) — is only valid when t is 'free for x in φ,' meaning no free variable of t would be captured. Without this condition, valid sentences can yield false conclusions: from the true ∀x ∃y (x ≠ y), naively instantiating with term y gives ∃y (y ≠ y), which is false. The free-for condition is not a technicality; it is what preserves the soundness of the proof system.

The deeper point is that bound variable names are arbitrary labels, not meaningful references. When a free variable in a substituted term 'accidentally' shares a name with a bound variable, the name collision corrupts the intended referential structure of the formula. Capture-avoidance — via α-renaming — ensures that substitution always produces a formula that means what it was intended to mean.