In the entry first-order language, 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 $\varphi$ if and only if it is not within the ``scope'' of a quantifier. For instance, $x$ occurs free in $\varphi$ if and only if it occurs in it as a symbol, and no subformula of $\varphi$ 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.

The set $FV(\varphi)$ of free variables of $\varphi$ is defined by well-founded induction on the construction of formulas. First we define $Var(t)$ , where $t$ is a term, to be the set or all variables occurring in $t$ , and then : \begin{eqnarray*} FV(t_1=t_2) & = & Var(t_2)\cup Var(t_2) \\ FV(R(t_1,...,t_n)) & = & \bigcup_{k=1}^n Var(t_k) \\ FV(\neg\varphi) & = & FV(\varphi) \\ FV(\varphi\Or\psi) & = & FV(\varphi)\cup FV(\psi) \\ FV(\exists x(\varphi)) & = & FV(\varphi)\backslash\{x\} \end{eqnarray*}When for some $\varphi$ , the set $FV(\varphi)$ is not empty, then it is customary to write $\varphi$ as $\varphi(x_1,...x_n)$ , in order to stress the fact that there are some free variables left in $\varphi$ , and that those free variables are among $x_1,...,x_n$ . When $x_1,...,x_n$ appear free in $\varphi$ , 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 $\varphi$ . If $FV(\varphi)=\emptyset$ , then $\varphi$ is called a sentence.

If a variable never occurs free in $\varphi$ (and occurs as a symbol), then we say the variable is bound. Bound variables can be inductively defined as well: let $\varphi$ be a formula, then we define the set $BV(\varphi)$ of bound variables as follows: \begin{eqnarray*} BV(\varphi) & = & \varnothing \quad \mbox{if }\varphi \mbox{ is an atomic formula}\\ BV(\neg\varphi) & = & BV(\varphi) \\ BV(\varphi\Or\psi) & = & BV(\varphi)\cup BV(\psi) \\ BV(\exists x(\varphi)) & = & BV(\varphi)\cup \{x\} \end{eqnarray*}Thus, a variable $x$ is bound if and only if $\exists x(\psi)$ or $\forall x(\psi)$ is a subformula of $\varphi$ for some $\psi$

Note that it is possible for a variable to be both free and bound. For example, consider the following formula $\varphi$ of the lenguage $\{+,\cdot,0,1\}$ of ring theory :

Lemma 1. It is possible to rename the bound variables without affecting the truth of a formula. In other words, if $\varphi=\exists x(\psi)$ , or $\forall x(\psi)$ , and $z$ is a variable not occurring in $\psi$ , then $\proves \varphi\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$ .