5.2  Terms, Formulas, Free Variables and Substitution

Section 5.1 read quantified sentences by eye. That is enough to understand them, and not enough to reason with them: every quantifier rule of Sections 5.3 to 5.6, and the rule for using an equation in Section 5.7, has the form “put the term $t$ in for the variable $x$ in $\phi$”, written $\phi [t/x]$, and a rule has to say exactly which symbols change. This section makes the language of Section 5.1 exact, in the way Section 4.1 made the propositional language exact, says exactly what $\phi [t/x]$ does, and names the one way it goes wrong, capture.

5.2.1. Which letters are holes

Three sentences, over the domain $\mathbb{N}$:

• “$x>2$” is not a statement. It is the open sentence of item (e) of Example (Statements and nonstatements), true for some values of $x$ and false for others.
• “$\mathrm{\forall }x(x^2\ge 0)$” is a statement, and a true one. The letter $x$ still appears, but the quantifier has closed its hole: the sentence does not ask which $x$ we mean.
• “$\mathrm{\forall }x(x\ge y)$” is neither true nor false as it stands. It is true when $y$ is $0$ (every natural number is at least $0$) and false when $y$ is $1$ (the number $0$ is not at least $1$). It is an open sentence in $y$, although it begins with a quantifier.

So the question “is this a statement?” is not answered by looking for quantifiers. It is answered by asking which letters are still holes. In the third sentence $x$ is closed by $\mathrm{\forall }x$ and $y$ is open. The open letters will be called free, and the closed ones bound.

Here is why the difference matters for reasoning. Over $\mathbb{N}$, the sentence $$\mathrm{\exists }y(y\ne x)$$ is an open sentence in $x$, and it is true for every $x$: given $x$, the number $y=x+1$ differs from it. Now suppose that we want to say the same thing about a particular number named by another letter, and we put $y$ in for $x$ without thinking. The result is $$\mathrm{\exists }y(y\ne y),$$ “some number differs from itself”, which is false. Nothing about numbers went wrong. The $y$ that we put in landed inside the scope of $\mathrm{\exists }y$, and the quantifier took hold of it: the new $y$ was meant to name a number from outside, and it has become the quantifier’s own placeholder. This is capture.

Capture is the one trap of substitution, and the rules of Sections 5.3 to 5.7 substitute at almost every step. So we need exact answers to three questions: what the expressions are that can be put in; which occurrences of $x$ get replaced; and when putting $t$ in for $x$ is safe.

5.2.2. Terms and formulas

The first things to build are the names of objects.

A term is a name of an object, built from variables and constants by function symbols.

In words: variables and constants are terms, a function symbol applied to as many terms as it has places is a term, and nothing else is.

A variable of a term $t$ is a variable that occurs in $t$. A term with no variables, such as $2$ or $f(c)$, names one fixed object once the symbols are interpreted; a term with variables, such as $x+1$, names an object only once its variables have values.

Shorthand. We write terms in the familiar way: $x+y$ for $+(x,y)$, $x^2$, $\left|x\right|$, $a_n$ for $a(n)$ (a sequence is a function symbol, as Section 5.1 said). School conventions about grouping say which term is meant.

Here are terms, simplest first.

• $x$ and $2$: by (Tm1). The degenerate terms, built in no steps; every argument about all terms has to handle them.
• $x+1$, officially $+(x,1)$: by (Tm2) from the terms $x$ and $1$.
• $f(f(c))$: by (Tm2) twice, from $c$, for a one-place $f$. Its only building blocks are constants, so it has no variables.
• $|a_n-L|$, officially $|\cdot |(-(a(n),L))$, with the two-place minus: by (Tm2) three times, from the variables $n$ and $L$. Its variables are $n$ and $L$. The letter $a$ is a function symbol, not a variable.

Next, the statements and open sentences. Atomic formulas say something about terms; everything else is built from them by connectives and quantifiers.

A first-order formula is built from predicates applied to terms, by the connectives and the two quantifiers.

• (Fm1): the atomic formulas, a predicate symbol with its terms, or an equation, or $\mathrm{\perp }$, take the place of Chapter 4’s atoms.
• (Fm2), (Fm3): the connectives, as before.
• (Fm4): puts $\mathrm{\forall }x$ or $\mathrm{\exists }x$, with a variable $x$, in front of a formula, without parentheses, as $\mathrm{\neg }$ is.

Structural induction and recursion (Theorem 4.3.1, Theorem 4.3.4) carry over to terms and first-order formulas, with the atomic formulas as base case and one new building step for each quantifier (the fold below says how).

Shorthand. The conventions of Section 4.1 for dropping parentheses stay, with three additions. Rules 1 and 3 (predicate symbols written between their terms, as in $x<y$; bounded quantifiers as abbreviations) are in the fold on the symbols of the language, above; rule 2 matters in every section:

Rule 2. A quantifier binds as tightly as $\mathrm{\neg }$: it applies to the smallest formula that follows it. So $\mathrm{\forall }xP(x)\to Q(c)$ stands for $(\mathrm{\forall }xP(x)\to Q(c))$, an implication whose hypothesis is $\mathrm{\forall }xP(x)$. For the quantifier to govern the whole implication, write $\mathrm{\forall }x(P(x)\to Q(x))$, where the parentheses are the official ones around the implication.

Rule 2 matters in every rule section. The formula $\mathrm{\forall }xP(x)\to Q(c)$ has main connective $\to$, while $\mathrm{\forall }x(P(x)\to Q(x))$ has main symbol $\mathrm{\forall }x$. The rule for using a “for every” (Section 5.3) applies only to the second.

Parse trees. A parse tree for a first-order formula is drawn as in Section 4.1, with one new kind of node: a quantifier node, labeled $\mathrm{\forall }x$ or $\mathrm{\exists }x$, with the tree of the formula it governs as its only subtree. The leaves are atomic formulas (or $\mathrm{\perp }$); their terms have trees of their own, which we do not draw. Here is the tree of $\mathrm{\forall }x(P(x)\to \mathrm{\exists }yR(x,y))$.

The root is the quantifier node $\mathrm{\forall }x$, so the formula’s main symbol is $\mathrm{\forall }x$. Below it is the implication, with the atomic formula $P(x)$ on the left and the quantifier node $\mathrm{\exists }y$ on the right, which governs the atomic formula $R(x,y)$.

5.2.3. Free and bound: drawing the arrows

The parse tree shows which quantifier governs which part of a formula. That is exactly what decides whether a letter is a hole. Draw an arrow from each occurrence of a variable to the nearest quantifier on that variable above it in the parse tree. An occurrence with an arrow is bound; one with none is a hole still open.

Figure B. Each bound occurrence points to its quantifier. The first $x$ points nowhere: it is free.

An occurrence of a variable is bound if a quantifier on that variable stands above it in the parse tree; otherwise it is free.

A variable appears in $\phi$ if it is written anywhere in $\phi$: inside a term, or just after a quantifier symbol. Every freshness condition of this chapter is stated with “appear”; in practice, a fresh letter is one written nowhere yet.

A sentence is what Chapter 1 called a statement, once the domain and the symbols are fixed: every hole is closed, so it is true or false. A formula with free variables is an open sentence, true or false only once values are given to its free variables.

Examples. The domain is irrelevant to all of them: being free or bound is a matter of the string, not of what it means.

• $\mathrm{\forall }x(x\ge y)$: the occurrence of $x$ is bound by $\mathrm{\forall }x$; the occurrence of $y$ has no quantifier on $y$ above it, so it is free. The free variables are $y$ alone. Not a sentence.
• $P(x)\wedge \mathrm{\forall }xQ(x)$: the occurrence of $x$ in $P(x)$ is free (no quantifier stands above it: the $\mathrm{\forall }x$ governs only $Q(x)$), and the occurrence in $Q(x)$ is bound. So $x$ is a free variable of this formula, and it is not a sentence.
• $\mathrm{\forall }x\mathrm{\exists }xP(x)$: the occurrence of $x$ has two quantifiers on $x$ above it, and the lower one, $\mathrm{\exists }x$, binds it. The outer $\mathrm{\forall }x$ binds nothing. A sentence.

5.2.4. Substitution, by example first

We now come to the operation that every quantifier rule uses. The rule of Section 5.3 will take the premise $\mathrm{\forall }x(P(x)\to S(x))$ of Section 5.1’s argument and produce $P(2)\to S(2)$: it strips the quantifier and puts $2$ in for $x$. The rule of Section 5.5 goes the other way. Both need to say exactly what “put $2$ in for $x$” does. The answer has one principle: only the free occurrences are replaced, because only they are holes. A bound occurrence belongs to its quantifier, and the quantifier is not asking for a value.

$\phi [t/x]$ is $\phi$ with $t$ put in for every free occurrence of $x$, and nothing else changed.

Here are the clauses those computations followed.

A compound term is written in parentheses: $\phi [(y+1)/x]$ puts $y+1$ in for $x$.

Two facts follow from the definition at once, and both are used again and again.

First, $\phi [x/x]=\phi$: putting $x$ in for itself changes nothing. In each clause the replaced symbol is $x$ again.

Second, and more useful: if $x$ is not free in $\phi$, then $\phi [t/x]=\phi$, for every term $t$. Example (d) was one instance. Later sections use it; its proof, a structural induction, is in the fold below.

One substitution at a time. $\phi [t/x]$ replaces one variable. Two substitutions in a row are made one after the other, and the second acts on the result of the first. So $R(x,y)[y/x]$ is $R(y,y)$, and then $[x/y]$ turns it into $R(x,x)$, not into the swapped $R(y,x)$: the first step has already lost track of which $y$ was which. To swap two variables, go through a letter that appears nowhere: $[z/x]$, $[x/y]$, $[y/z]$ give $R(z,y)$, $R(z,x)$, $R(y,x)$.

5.2.5. Capture, and the practical rule

The definition of substitution never refuses. Given any $\phi$, $t$ and $x$, it returns a formula. Sometimes that formula does not say what we meant.

Take $\phi =\mathrm{\exists }y(y\ne x)$, the example at the start of the section, and $t=y$. The quantifier $\mathrm{\exists }y$ is on a variable different from $x$, so the definition passes the substitution through, and $$(\mathrm{\exists }y(y\ne x))[y/x]=\mathrm{\exists }y(y\ne y).$$ The definition was followed correctly. The meaning is wrong. The formula $\mathrm{\exists }y(y\ne x)$ says something about the number $x$: some number differs from it, which over $\mathbb{N}$ is true whatever $x$ is. We wanted to say the same thing about the number $y$, and we got “some number differs from itself”, which is false. The $y$ we put in was supposed to name a number from outside, and it landed in the scope of $\mathrm{\exists }y$ and was captured.

Compare a substitution that is safe. Over $\mathbb{R}$, $\mathrm{\forall }z(x<z)$ says that $x$ is smaller than every number (false, as it happens, for every $x$; but what matters is what it says). Put $y+1$ in for $x$: the quantifier $\mathrm{\forall }z$ passes the substitution on, and $$(\mathrm{\forall }z(x<z))[(y+1)/x]=\mathrm{\forall }z(y+1<z),$$ which says exactly that $y+1$ is smaller than every number. Nothing was captured, because the term $y+1$ does not contain $z$, the only variable quantified above the occurrence of $x$.

The difference between the safe case and the unsafe one is exactly this: whether a variable of $t$ is quantified somewhere above a free occurrence of $x$.

A term is free for $x$ when putting it in for $x$ lets none of its variables be captured.

In words: look at each place where $t$ will go, that is, at each free occurrence of $x$. Look at the quantifiers above it in the tree. If none of them is on a variable of $t$, the substitution is safe there. The term is free for $x$ when it is safe at every such place. Informally: no variable of $t$ becomes bound when $t$ is put in.

Four special cases, each immediate from the definition, cover most uses.

• A term with no variables ($2$, $c$, $f(c)$) is free for every variable in every formula: there is no $y$ to capture.
• The variable $x$ is free for $x$ in every formula. A free occurrence of $x$ never lies in the scope of a quantifier on $x$; if it did, it would be bound.
• A variable $z$ that does not appear in $\phi$ is free for every variable in $\phi$: no quantifier of $\phi$ is on $z$.
• If $x$ is not free in $\phi$, every term is free for $x$ in $\phi$: there are no free occurrences to check. (And then $\phi [t/x]=\phi$ by the claim above.)

In our examples: $y$ is not free for $x$ in $\mathrm{\exists }y(y\ne x)$, because the free occurrence of $x$ lies in the scope of $\mathrm{\exists }y$ and $y$ is a variable of the term $y$. Likewise $y+1$ is not free for $x$ in $\mathrm{\exists }y(y>x)$. And $y+1$ is free for $x$ in $\mathrm{\forall }z(x<z)$: the only quantifier above the free occurrence of $x$ is on $z$, which is not a variable of $y+1$.

“Free for” is the precise condition under which $\phi [t/x]$ says about $t$ what $\phi$ says about $x$. The rules $\mathrm{\forall }\mathrm{E}$ (Section 5.3), $\mathrm{\exists }\mathrm{I}$ (Section 5.5) and $=\mathrm{E}$ (Section 5.7) carry it as a side condition.

Before you substitute. Look at each free occurrence of $x$ and at the quantifiers above it. If none of them is on a letter of $t$, go ahead. If one is, rename that quantifier’s letter to a brand-new letter first (next subsection), and then substitute. Nothing else can go wrong.

5.2.6. Renaming bound variables

What should we do when $t$ is not free for $x$ in $\phi$? A bound variable is a placeholder, and the name of a placeholder does not matter. “Some number differs from $x$” can be written $\mathrm{\exists }y(y\ne x)$ or $\mathrm{\exists }z(z\ne x)$, just as ${\int }_0^1{s}^{2}ds$ and ${\int }_0^1{u}^{2}du$ are the same integral. So the way out is: rename the bound variable first, then substitute.

Renaming. Let $\phi$ be a formula and $y,z$ variables, with $z$ not appearing in $\phi$. The formula $\mathrm{\forall }z\phi [z/y]$ is obtained from $\mathrm{\forall }y\phi$ by renaming the bound variable $y$ to $z$; likewise $\mathrm{\exists }z\phi [z/y]$ from $\mathrm{\exists }y\phi$. The same may be done to a quantifier anywhere inside a larger formula.

In words: change the variable after the quantifier, and change the occurrences it binds, to a letter that appears nowhere in the formula. The condition that $z$ does not appear in $\phi$ does two jobs. It makes $z$ free for $y$ in $\phi$ (the third special case above), so no new $z$ is captured by a quantifier inside $\phi$. And it ensures that no free $z$ already in $\phi$ is captured by the new quantifier $\mathrm{\forall }z$. Without it, renaming can change the meaning: $\mathrm{\forall }y(y\ge z)$ says something about $z$ (over $\mathbb{N}$, that $z=0$), and “renaming” $y$ to $z$ would give $\mathrm{\forall }z(z\ge z)$, a sentence that is simply true.

Renaming a bound letter is treated as never changing what a formula says; Sections 5.4 and 5.6 derive it at the front of a formula, and the fold says where the rest stands.

The recipe. To put $t$ in for $x$ in $\phi$ when $t$ is not free for $x$: rename each quantifier of $\phi$ that is on a variable of $t$ and has a free occurrence of $x$ in its scope, each to a different variable that appears neither in $\phi$ nor in $t$ (each such step is a renaming in the sense above); then substitute. After the renaming, $t$ is free for $x$.

• $\mathrm{\exists }y(y\ne x)$ with $y$ for $x$: rename $y$ to $z$, giving $\mathrm{\exists }z(z\ne x)$; then substitute, giving $\mathrm{\exists }z(z\ne y)$, “some number differs from $y$”. True over $\mathbb{N}$ for every $y$, as intended.
• $\mathrm{\exists }y(y>x)$ with $y+1$ for $x$: rename to $\mathrm{\exists }z(z>x)$; substitute, giving $\mathrm{\exists }z(z>y+1)$. True over $\mathbb{R}$, as intended.

Which fresh letter we choose does not matter: two choices give formulas that differ only by a renaming. From now on, whenever a rule writes $\phi [t/x]$, it will require $t$ to be free for $x$ in $\phi$, and if we want a $t$ that is not, we rename first.

5.2.7. How substitution looks in a mathematical proof

Mathematicians substitute constantly and never write $[t/x]$. Two examples show the operation, and its trap, in their natural habitat.

“Apply the hypothesis with $\epsilon /2$ in place of $\epsilon$.” Suppose we know that $(a_n)$ converges to $L$, and we have fixed an $\epsilon >0$ for some other purpose. A proof says: “applying the hypothesis with $\epsilon /2$, there is an $N\in \mathbb{N}$ with $|a_n-L|<\epsilon /2$ for all $n\ge N$”. The hypothesis is $\mathrm{\forall }\epsilon \phi$, with $$\phi =(\epsilon >0\to \mathrm{\exists }N\in \mathbb{N}\mathrm{\forall }n\in \mathbb{N}(n\ge N\to |a_n-L|<\epsilon )),$$ and the proof uses the instance $\phi [t/\epsilon ]$ with the term $t=\epsilon /2$: $$\epsilon /2>0\to \mathrm{\exists }N\in \mathbb{N}\mathrm{\forall }n\in \mathbb{N}(n\ge N\to |a_n-L|<\epsilon /2).$$ The term $\epsilon /2$ contains the variable $\epsilon$: the fixed $\epsilon$ of the proof, not the bound one of the hypothesis. It is free for $\epsilon$ in $\phi$, because the only quantifiers above the free occurrences of $\epsilon$ in $\phi$ are on $N$ and $n$. Section 5.3’s rule makes this step, and “$\epsilon /2>0$” then comes from $\epsilon >0$ by arithmetic.

“Take $N=n$.” Now suppose the proof has chosen $N$, so it knows $$\psi =\mathrm{\forall }n\in \mathbb{N}(n\ge N\to |a_n-L|<\epsilon ),$$ with $N$ free. A tempting step is to “apply this with $n$ in place of $N$”. No rule allows this: $N$ has been chosen, not quantified, so no term may be put in for it. Writing the step out shows how badly it goes wrong, because $n$ is not even free for $N$ in $\psi$: the occurrence of $N$ lies in the scope of $\mathrm{\forall }n$. The substitution produces $$\mathrm{\forall }n\in \mathbb{N}(n\ge n\to |a_n-L|<\epsilon ),$$ which says that every term of the sequence is within $\epsilon$ of $L$, a far stronger claim that does not follow. In words, the error is to let the threshold $N$ be “the $n$ we are looking at”, when $n$ is the placeholder of “for all $n\ge N$”. A proof that needs a statement about a particular index names it with a new letter, say $m\ge N$, and substitutes $m$, which is free for $n$.

5.2.8. Exercises

A. Check your understanding