Free and Bound Variables: Read Scope Without Capturing a Variable

Classify occurrences, rather than variable letters alone

A variable occurrence is bound when it lies in the scope of a quantifier for that variable. When quantifiers for the same variable are nested, the closest enclosing binder controls the occurrence. An occurrence with no such binder is free.

One formula can contain a bound x in one place and a free x elsewhere. So “x is a bound variable” can be misleading unless you identify the occurrence. A formula with free occurrences is open; its satisfaction depends on an assignment of objects to those free variables. A sentence has no free occurrences.

Definitions and rules: [2] [1].

(∀xRxy) ∧ Px

Annotate the three occurrences in one formula

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

The parentheses end the first quantifier’s scope before the conjunction. They do not let ∀x reach across and bind the x in Px. Merely being somewhere in a quantified formula is not sufficient: y lies inside that scope but is not bound by a quantifier for x.

For comparison, ∀x(Rxy∧Px) binds both x occurrences, while y remains free. Adding ∀y outside that entire formula would bind y as well. Use explicit parentheses whenever you are uncertain about the textbook’s conventions for omitting them.

Evaluate the open formula under complete assignments

Here is a deliberately constructed interpretation: D={A,B}, P={A}, and R={(A,A),(B,A)}. These are all the true relation pairs; R(A,B) and R(B,B) are false. Let an assignment specify x and y for the free occurrences.

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

Download the complete interpretation and occurrence annotations

For y=A, the universal part tests R(A,A) and R(B,A), both true. Its bound x ranges over the whole domain, rather than taking the free x’s assigned value. The separate Px is true only when the free x is assigned A. With y=B, the universal part fails regardless of the free x assignment.

Thus an unassigned open formula does not supply a single closed-sentence truth value. Once you supply the interpretation and assignment, its satisfaction can be checked. Do not confuse that dependence with missing or third-valued relation data.

Definitions and rules: [1].

Rename only the occurrences controlled by your chosen binder

Safe:
(∀xRxy) ∧ Px  →  (∀zRzy) ∧ Px

Capture changes meaning:
∀xRxy  →  ∀yRyy

The safe change uses a fresh z and replaces just the bound x in Rxy. It leaves the free x in Px and the free y untouched. Both formulas consequently have the same satisfaction under each assignment in the table.

The second change is unsafe. The y that was free has fallen under the new ∀y binder. In our interpretation, the original ∀xRxy is true when free y is A, but ∀yRyy is false because R(B,B) is false. Variable capture changes the question being evaluated.

Before renaming, mark the binder’s full scope, exclude occurrences governed by an inner binder for the same variable, and choose a name not occurring in the target scope. Then replace only the selected bound occurrences. A fresh name is a simple way to avoid both capture of free occurrences and conflicts with inner binders.

Read legal rebinding and vacuous quantification carefully

Legal inner rebinding:
∀x(Px ∧ ∃xQx)

In this formula, the x in Px belongs to the outer ∀x, while the x in Qx belongs to the inner ∃x. The inner quantifier does not change the x occurrence already written in Px. The cited syntax chapter explicitly permits this nearest-binder structure, even though it is harder to read.

Renaming the inner binder with a fresh y gives ∀x(Px∧∃yQy). Renaming the outer binder instead gives ∀z(Pz∧∃xQx). Do not mechanically replace every x in the original formula, because the two binders control different occurrences.

Definitions and rules: [2].

A quantifier can also be vacuous, as in ∀xQy: its scope contains no x occurrence to bind. It does not bind y. In the nonempty-domain semantics used here, this open formula has the same satisfaction as Qy under an assignment. Being syntactically allowed does not make redundant quantification good explanatory notation.

Try three scope checks

Track the individual occurrence and the nearest matching binder.