free and bound variables

In the entry first-order language (http://planetmath.org/TermsAndFormulas), I have mentioned the use of variables without mentioning what variables really are. A variable is a symbol that is supposed to range over the universe of discourse. Unlike a constant, it has no fixed value.

There are two ways in which a variable can occur in a formula: free or bound. Informally, a variable is said to occur free in a formula $\phi$ if and only if it is not within the “scope” of a quantifier. For instance, $x$ occurs free in $\phi$ if and only if it occurs in it as a symbol, and no subformula of $\phi$ is of the form $\exists x.\psi$. Here the $x$ after the $\exists$ is to be taken literally : it is $x$ and no other symbol.

Variables in Terms

To formally define free (resp. bound) variables in a formula, we start by defining variables occurring in terms, which can be easily done inductively: let $t$ be a term (in a first-order language), then $\mathrm{Var}(t)$ is

• if $t$ is a variable $v$, then $\mathrm{Var}(t)$ is $\{v\}$

• if $t$ is $f(t_1,\mathrm{\dots },t_n)$, where $f$ is a function symbol of arity $n$, and each $t_i$ is a term, then $\mathrm{Var}(t)$ is the union of all the $\mathrm{Var}(t_i)$.

Free Variables

Now, let $\phi$ be a formula. Then the set $\mathrm{FV}(\phi )$ of free variables of $\phi$ is now defined inductively as follows:

• if $\phi$ is $t_1=t_2$, then $\mathrm{FV}(\phi )$ is $\mathrm{Var}(t_1)\cup \mathrm{Var}(t_2)$,

• if $\phi$ is $R(t_1,\mathrm{\dots },t_n)$, then $\mathrm{FV}(\phi )$ is $\mathrm{Var}(t_1)\cup \mathrm{\cdots }\cup \mathrm{Var}(t_n)$

• if $\phi$ is $\mathrm{\neg }\psi$, then $\mathrm{FV}(\phi )$ is $\mathrm{FV}(\psi )$

• if $\phi$ is $\psi \vee \sigma$, then $\mathrm{FV}(\phi )$ is $\mathrm{FV}(\psi )\cup \mathrm{FV}(\sigma )$, and

• if $\phi$ is $\exists x\psi$, then $\mathrm{FV}(\phi )$ is $\mathrm{FV}(\psi )-\{x\}$.

If $\mathrm{FV}(\phi )\ne \mathrm{\varnothing }$, it is customary to write $\phi$ as $\phi (x_1,\mathrm{\dots },x_n),$ in order to stress the fact that there are some free variables left in $\phi$, and that those free variables are among $x_1,\mathrm{\dots },x_n$. When $x_1,\mathrm{\dots },x_n$ appear free in $\phi$, then they are considered as place-holders, and it is understood that we will have to supply “values” for them, when we want to determine the truth of $\phi$. If $\mathrm{FV}(\phi )=\mathrm{\varnothing }$, then $\phi$ is called a sentence. Another name for a sentence is a closed formula. A formula that is not closed is said to be open.

Bound Variables

Bound variables in formulas are inductively defined as well: let $\phi$ be a formula. Then the set $\mathrm{BV}(\phi )$ of bound variables of $\phi$

• if $\phi$ is an atomic formula, then $\mathrm{BV}(\phi )$ is $\mathrm{\varnothing }$, the empty set,

• if $\phi$ is $\mathrm{\neg }\psi$, then $\mathrm{BV}(\phi )$ is $\mathrm{BV}(\psi )$

• if $\phi$ is $\psi \vee \sigma$, then $\mathrm{BV}(\phi )$ is $\mathrm{BV}(\psi )\cup \mathrm{BV}(\sigma )$, and

• if $\phi$ is $\exists x\psi$, then $\mathrm{BV}(\phi )$ is $\mathrm{BV}(\psi )\cup \{x\}$.

Thus, a variable $x$ is bound in $\phi$ if and only if $\exists x\psi$ is a subformula of $\phi$ for some formula $\psi$.

The set of all variables occurring in a formula $\phi$ is denoted $\mathrm{Var}(\phi )$, and is $\mathrm{FV}(\phi )\cup \mathrm{BV}(\phi )$.

Note that it is possible for a variable to be both free and bound. In other words, $\mathrm{FV}(\phi )$ and $\mathrm{BV}(\phi )$ are not necessarily disjoint. For example, consider the following formula $\phi$ of the lenguage $\{+,\cdot ,0,1\}$ of ring theory :

$$x+1=0\wedge \exists x(x+y=1)$$

Then $\mathrm{FV}(\phi )=\{x,y\}$ and $\mathrm{BV}(\phi )=\{x\}$: the variable $x$ occurs both free and bound. However, the following lemma tells us that we can always avoid this situation :

Lemma 1. It is possible to rename the bound variables without affecting the truth of a formula. In other words, if $\phi =\exists x(\psi )$, or $\forall x(\psi )$, and $z$ is a variable not occurring in $\psi$, then $⊢\phi \iff \exists z(\psi [z/x])$, where $\psi [z/x]$ is the formula obtained from $\psi$ by replacing every free occurrence of $x$ by $z$.

As a result of the lemma above, we see that every formula is logically equivalent to a formula $\phi$ such that $\mathrm{FV}(\phi )\cap \mathrm{BV}(\phi )=\mathrm{\varnothing }$.