The Gold Standard of Mathematical Logic | Bound Variables, Renaming and Variable Capture

A variable occurrence is bound when it lies within the scope of a quantifier for that variable, with the appropriate nearest binder. An occurrence is free when no such binder governs it.

In ∀x R(x,y), the occurrence of x inside R is bound by ∀x. The occurrence of y is free. The quantifier specifies how x ranges through the domain, while a variable assignment supplies the current value of y.

The same letter can have both free and bound occurrences in a larger formula. In (∀x P(x)) ∧ Q(x), the x inside P is bound, while the x inside Q is free. The parentheses end the first quantifier’s scope before Q(x).

Saying simply “x is bound” can therefore conceal an important distinction. Point to the occurrence, or specify the subformula being discussed.

A simple scope annotation

Draw a boundary around the subformula following each quantifier. Connect each governed occurrence to that quantifier. Leave free occurrences unconnected. If an inner quantifier uses the same variable letter, it takes over the occurrences within its own scope.

For ∀x(P(x) ∧ ∃x Q(x)), the outer ∀x binds the x in P. The inner ∃x binds the x in Q. The inner use shadows the outer one; it does not mean the two quantified objects must be identical.

This is legal syntax in many presentations, but it can be hard to read. Renaming the inner variable to a fresh letter yields ∀x(P(x) ∧ ∃z Q(z)), making the separate roles clearer.

A careful reader checks the syntactic structure before supplying a story. A plausible story cannot repair a scope boundary that has been misread.

Contents · Next chapter

An open formula has at least one free variable occurrence. For example, R(x,a) has free x and a constant symbol a. An interpretation assigns an object to a, while an assignment supplies a value for x.

A sentence such as ∀x R(x,a) has no free variables. Its truth depends on the interpretation but not on which object an assignment initially gives x, because the quantifier ranges over x.

For an original arithmetic example over the integers, let P(x) mean x > 2. Under an assignment x = 5, P(x) is true. Under x = 1, it is false. There is no contradiction: the free variable has received different values.

The universal closure ∀x P(x) is false over the integers. The existential closure ∃x P(x) is true. Adding a quantifier is therefore a substantive assertion, not merely punctuation that makes a formula look complete.

Free-variable sets

For R(x,y), the free-variable set is {x,y}. For ∀x R(x,y), it is {y}. For (∀x P(x)) ∧ Q(x), it is {x}, because the second occurrence remains free.

This set is useful for identifying whether a formula is a sentence, but it does not replace an occurrence-level map. A variable may appear in the set even when some of its occurrences are bound.

When an exercise asks whether a formula is true, check whether it supplies an assignment for the free variables. If not, it may instead be asking whether the formula is true under every assignment or whether some assignment satisfies it.

These are different questions. State which one is being assessed before returning a true-or-false verdict.

Contents · Previous chapter · Next chapter

Bound-variable renaming is often called alpha-renaming. In ∀x R(x,y), changing the binder x and its governed occurrences to a fresh z gives ∀z R(z,y). The formula makes the same demand.

The free y stays free. Only occurrences governed by the selected binder are renamed. A mechanical replacement of every x in a larger expression can change unrelated occurrences.

For example, in (∀x P(x)) ∧ Q(x), renaming the first binder gives (∀z P(z)) ∧ Q(x). Replacing Q(x) with Q(z) as well would change a free variable and therefore change which assignment is consulted.

Freshness protects existing roles

Consider ∀x R(x,z). Renaming the bound x to z would give ∀z R(z,z). The originally free z has become bound. This is variable capture, and the transformation is not generally meaning-preserving.

A fresh letter such as w gives ∀w R(w,z), preserving the free z and the original dependency.

Fresh means suitable for the relevant scope, not merely different from the old binder. A letter already bound by an inner quantifier or occurring free in the body can create trouble. Choosing a letter absent from the whole formula is a convenient sufficient precaution for elementary work.

Renaming also must respect shadowing. In ∀x(P(x) ∧ ∃x Q(x)), changing the outer binder to w changes P(x) to P(w), but leaves the inner ∃x Q(x) untouched. Its x-occurrences belong to the inner binder.

A good explanation names exactly which binder is being changed and which occurrences travel with it. “Replace x by w everywhere” is too crude unless the formula has already been checked to make that instruction safe.

Contents · Previous chapter · Next chapter

Take the open formula φ(x) = ∀y R(x,y). Its free x identifies an object related to every domain object. Suppose we want to substitute the free variable y for x.

Naively replacing x gives ∀y R(y,y). This binds the inserted y and asks whether every object relates to itself. It is a different property.

To avoid capture, first rename the original bound y to a fresh z: ∀z R(x,z). Then substitute y for the free x, giving ∀z R(y,z). The inserted y stays free.

Verify the difference

Let the domain be {0,1}, with R = {(0,0),(0,1)}. Give the free y the value 0. The correctly substituted formula ∀z R(y,z) is true: 0 relates to both 0 and 1.

The captured formula ∀y R(y,y) is false because R(1,1) is false. The attempted edit has changed truth in a fully specified interpretation.

The counterexample is decisive because a meaning-preserving transformation must agree in every relevant interpretation and assignment. Agreement in one convenient example would not establish that the edit was safe.

The lesson is also visual. Before substitution, one input slot is supplied by the assignment and another is ranged over by a quantifier. After capture, both slots are controlled by the same quantifier. The letters may look tidy while the dependency has changed.

Contents · Previous chapter · Next chapter

Substitution for a free variable does not rewrite occurrences of the same letter that are bound by a quantifier. Consider R(x,y) ∧ ∀x S(x,y). Substitute constant a for free x.

The result is R(a,y) ∧ ∀x S(x,y). The first x was free; the x inside S is governed by ∀x and remains unchanged.

Substituting a constant does not introduce a variable that a quantifier could capture, because a constant symbol is not a variable. But the target-occurrence restriction still matters.

Terms can contain several variables

If the language includes a function symbol f, a term such as f(y,z) may be substituted for x. Its free variables must remain free where the term is inserted. A surrounding ∀y or ∃z can make direct insertion unsafe.

For ∃z T(x,z), substituting f(y,z) for x would naively produce ∃z T(f(y,z),z). The z inside the inserted term has become bound. Rename the original binder first: ∃w T(x,w), then substitute to obtain ∃w T(f(y,z),w).

The function symbol’s interpretation determines the value of the term, but variable capture is a syntactic problem that can be detected before those values are known.

Some textbooks define substitution only when the term is free for the variable in the formula. Others define a capture-avoiding substitution operation that performs necessary renaming. These conventions express related safeguards but should not be conflated.

In a written solution, show the fresh renaming step explicitly. This makes the operation inspectable and avoids relying on an unstated software or textbook convention.

Contents · Previous chapter · Next chapter

Compare ∀x(P(x) → Q(x)) with (∀x P(x)) → Q(x). In the first, both occurrences are bound. In the second, the x in Q is free. The parentheses change the outer logical structure as well as the variable dependencies.

Over domain {0,1}, let P be true only of 0, and Q be false of both objects. The first formula is false because at x = 0 the antecedent is true and consequent false.

The second formula is true under every assignment: ∀x P(x) is false, so the material conditional holds regardless of Q(x). These formulas are not interchangeable.

Read the main connective first

For the first expression, the whole formula begins with a universal quantifier. For the second, the main connective is an implication between a universally quantified antecedent and an open consequent.

A helpful parsing routine is to identify the outermost operator, then recursively inspect its components. Only after that should the reader determine which quantifier binds each occurrence.

This routine also prevents an editing error in prose translation. “Everyone who submitted a form received a reply” is naturally represented with the universal covering the conditional. Moving the quantifier into the antecedent creates a different claim.

Avoid relying on visual proximity alone. A variable beside a quantifier may remain outside its scope because a parenthesis has closed; a distant occurrence may remain within its scope.

When notation omits optional parentheses by convention, state the convention before interpreting an unfamiliar formula. Fully parenthesised expressions are useful during learning because they remove an avoidable source of disagreement.

Contents · Previous chapter · Next chapter

From ∀x P(x), a proof may infer P(a), with a denoting an object in the domain. More generally, universal instantiation replaces free occurrences of the quantified variable in the body with a suitable term.

The suitability condition prevents capture. From ∀x∀y R(x,y), substituting a constant a for the outer x gives ∀y R(a,y). This is safe.

For a variable term y, direct substitution into the outer body ∀y R(x,y) is unsafe. Rename the inner binder to z before obtaining ∀z R(y,z). The original universal sentence really does support this open instance under standard semantics; the issue is preserving the intended substitution.

An assignment-level check

A universal statement must hold for every domain value of x. If the current assignment gives y a particular object, the universal statement holds with x taking that object’s value. The remaining inner quantifier must still range independently.

The captured expression ∀y R(y,y) may happen to follow from ∀x∀y R(x,y), but that does not make capture a valid substitution operation. It has produced a different instance, and an accidental success in a stronger premise does not justify the general editing rule.

This distinction is useful in proof checking. A line can be a consequence of earlier premises while its written justification is incorrect. A complete proof needs both a true consequence and a rule application that actually licenses the displayed step.

The repair is to separate semantic consequence from syntactic substitution. Show the fresh binder, perform the permitted replacement, and only then invoke the proof rule. That sequence keeps the proof auditable.

Contents · Previous chapter · Next chapter

A safe edit begins by finding the selected binder or free variable. Mark every target occurrence. List the variables occurring in the term to be inserted. Check whether any surrounding quantifier would capture them.

If capture is possible, rename the relevant bound variables to fresh letters, preserving their governed occurrences. Then perform the substitution and recompute the free-variable set.

For φ = ∀y R(x,y), free variables before substitution are {x}. Replacing free x by y should leave a result whose free-variable set is {y}. The captured result has no free variables, immediately revealing a likely problem.

This set check is useful but not sufficient by itself. Different incorrect formulas can have the same free-variable set. Follow it with an occurrence map and, when needed, a finite interpretation that tests the proposed equivalence.

Keep changes reviewable

Write one transformation per line with a reason: bound-variable renaming, free substitution or logical equivalence. Combining all three in one unexplained jump makes mistakes harder to locate.

In a classroom, preserve correct parts of the formula. If one inserted variable was captured, repair the binder and its scope rather than replacing the entire expression with a memorised pattern.

For computer representations, variable handling may use explicit binders, indexed variables or other techniques to prevent capture. The mathematical requirement remains the same: an edit must preserve which occurrences depend on which binders. This guide does not prescribe a particular implementation.

The learner’s final explanation should be concrete: “The new y remains free because the old bound y was renamed to z before insertion.” That shows control of the mechanism rather than recognition of a warning label.

Contents · Previous chapter · Next chapter

Exercise 1: mixed occurrences

Find the free variables in (∀x R(x,y)) ∧ S(x,z). The answer is {x,y,z}. The x in R is bound, but the x in S is free.

Exercise 2: safe renaming

Rename the bound x in ∀x R(x,z) to a fresh w. The result is ∀w R(w,z). Renaming it to z without further repair would capture the formerly free z.

Exercise 3: free substitution

In R(x,y) ∧ ∃x S(x,y), replace free x with constant a. The result is R(a,y) ∧ ∃x S(x,y). The inner bound x remains unchanged.

Exercise 4: avoid capture

Replace free x by y in ∃y R(x,y). First rename the binder: ∃z R(x,z). Then substitute to obtain ∃z R(y,z). Its free-variable set is {y}.

Exercise 5: test a bad edit

Let D = {0,1} and R = {(0,0),(0,1)}. Under y = 0, evaluate ∀z R(y,z) and ∀y R(y,y). The first is true; the second is false because R(1,1) fails.

Transfer check

Take a formula containing a quantifier and a free variable. Propose a substitution term that shares a variable with the binder. Show the unsafe edit, explain the capture, then repair it with fresh renaming.

Finish by identifying the free variables and evaluating both versions in a small model. If the unsafe edit happens to agree in that model, try a relation that separates a full row from the diagonal. One successful truth comparison cannot certify all possible edits.

Contents · Previous chapter · Next chapter

Frequently asked questions

Can the same variable letter be free and bound in one formula? Yes. Freedom and binding apply to occurrences within scopes.

Does renaming a bound variable always preserve meaning? Only when the renaming preserves the binding structure and avoids capture.

Can substituting a constant capture a variable? A constant introduces no variable occurrences to capture, but substitution must still target only the intended free occurrences.

Is a formula with no free variables a sentence? Yes, under the standard terminology used here.

Connected reading

Return to Mathematical Logic for syntax and proof systems. The existing quantifier-dependence guide explains which witness choices may depend on earlier variables. The countermodel guide develops the finite truth checks used here.

Sources and scope

Variable scope and sentence formation were checked against forall x: Calgary, Sentences of FOL. Term substitution and semantic conventions are developed in the Open Logic Project syntax and semantics reference. Accessed 22 October 2026. All finite examples and repair sequences here are original teaching constructions. Proof systems vary in notation; use the precise substitution convention specified by the system being studied.

Contents · Previous chapter · Continue to Mathematical Logic