Variable substitution in first-order logic is the operation of replacing free occurrences of a variable x in a formula φ with a term t, written φ[t/x]. Capture-avoidance is the critical constraint: if t contains variables, those variables must not become bound by quantifiers in φ. For example, substituting y for x in ∃y P(x, y) cannot naively give ∃y P(y, y) because y in t becomes captured. Proper substitution requires renaming bound variables in φ to avoid this. This technical detail is crucial for the correctness of proof rules and model-theoretic arguments.
Practice substitution on simple formulas, identifying when capture would occur. Understand that renaming bound variables preserves logical equivalence and allows safe substitution. Use concrete examples where capture-avoidance is essential (e.g., universal instantiation in proofs).
From your study of terms and formulas in first-order logic, you know that variables play two distinct roles: they appear free (as placeholders for arguments, ranging over the domain) or bound (tied to a quantifier, acting as a local name). Variable substitution — replacing free occurrences of a variable x with a term t — is the fundamental operation for instantiating quantifiers and making inferences about specific elements. Writing φ[t/x] means "φ with every free occurrence of x replaced by t."
The operation seems straightforward until the term t *contains variables*. Suppose φ is ∃y P(x, y), expressing "there exists something that stands in relation P to x." If we substitute y for x naively, we get ∃y P(y, y) — which says "there exists something that stands in P to itself," a completely different claim. The variable y in the substituted term has been captured by the quantifier ∃y inside φ, changing its meaning from "the external y we want to substitute" to "the locally bound variable of the quantifier." Capture corrupts the substitution — the resulting formula no longer means what we intended.
Capture-avoidance prevents this by requiring that no free variable in t becomes bound in φ[t/x]. The standard fix is α-renaming: before substituting, rename the bound variables in φ that would cause capture. In the example above, rename ∃y to ∃z to get ∃z P(x, z), and now substituting y for x correctly yields ∃z P(y, z), which says "there exists something standing in P to y" — exactly what we wanted. Renaming bound variables is always safe because α-equivalent formulas (differing only in bound variable names) are logically identical: ∀x P(x) and ∀y P(y) say exactly the same thing.
The practical consequence for proof rules is immediate. The universal instantiation rule — from ∀x φ(x), conclude φ(t) for any term t — only applies when t is free for x in φ, meaning no free variable of t would be captured by a quantifier in φ. This is not a pedantic restriction; it is what makes the inference valid. If you instantiate ∀x ∃y (x ≠ y) with the term y, you would (naively) get ∃y (y ≠ y), which is false — a valid sentence led to a false one, breaking the proof system. The free-for condition is the guard that prevents this. In practice, using ground terms (constants, with no variables) automatically satisfies capture-avoidance, which is why witness constants in the Henkin construction and other proof-theoretic arguments routinely substitute constants rather than arbitrary terms.