Free and bound variables

Consider the formula

$$Z=\{\forall _{x}\neg \mathrm{Cretan}(x)\vee \mathrm{liar}(x)\}$$

Inside this formula, is a variable. Outside this formula there are no variables -- because is doing an implied AND:

$$\begin{eqnarray*} Z & = & \neg \mathrm{Cretan}(\mathrm{Thing}_{1})\vee \mathrm{l... ...\vee \mathrm{liar}(\mathrm{Thing}_{2})\\ & \bigwedge & \vdots \end{eqnarray*}$$

So is successively set equal to all of the objects in the universe and a huge AND is taken. The variable is being used to perform a computation and no longer exists outside the formula -- it is said to be bound.

The same is true of variables that appear as subscripts to an quantifier, as the following example shows

$$\{\exists _{x}\mathrm{big}(x)\wedge \mathrm{dog}(x)\}$$

(``there exists a big dog''). Since an quantifier is performing an implied OR:

$$\begin{eqnarray*} & & \mathrm{big}(\mathrm{Thing}_{1})\wedge \mathrm{dog}(\math... ...)\wedge \mathrm{dog}(\mathrm{Thing}_{2})\\ & \bigvee & \vdots \end{eqnarray*}$$

so that the variable no longer exists outside the formula. Rule:

Variables that appear as subscripts to quantifiers are bound and do not exist outside their scope (the portion of the formula in which they appear).

Bound variables are like local variables to a subroutine or variables over which you are computing definite integrals. Variables that are not bound are said to be free. Example:

$$Z=\{\exists _{x}\mathrm{bigger}(x,y)\}$$

Since was not a subscript of a quantifies, it remains free. Consequently, is really a function of one variable, and we should have written

$$Z(y)=\{y\vert\exists _{x}\mathrm{bigger}(x,y)\}$$

It is true for a given if there exists something bigger than it (assuming that we have defined the predicate function in this way).