In the previous examples we often re-used variable names, even within the same formula. This shouldn't be surprising or confusing, since we do the same thing in programs (another formal
language). In fact, the same notions of **bound** and **free** variables occur in both situations. An occurrence of variable *x* is
bound if it is in the body of a quantifier ∀*x* ... or ∃*x* .... Otherwise, the occurrence is free.

For example, in ∀** x** : (

**likes**

**(**), the variable

*x*,*y*)*y*is free but

*x*is not. So this is a statement about

*y*; we can't evaluate this to true/false until we get some context for

*y*. It's useful as a subpart for some bigger formula.

*φ*" does not talk about the context of

*φ*. So don't confuse it with "well, over on this part of the page,

*φ*happens to occur as the sub-part of another formula containing ∀

*x*:(... ), so

*x*really is bound." (Just as 7 is prime, even though people sometimes use 7 in the context of 7+1.) Whether

*x*is free in a

*φ*can be determined by a function isFree (

*x*,

*φ*), needing no other information to produce an answer.

Looking back at our previous examples, we can see that many of the formulas we made had no free variables all variables were bound by some quantifier in the formula. The truth of such formulas
depends only on the interpretation and not on any additional knowledge about what any free variables refer to. Thus, these formulas are common and important enough that we give them a special
name, **sentences**.

A given variable name can actually have **both** bound and free occurrences within the same formula, as in *R* (*x***)** ∧∃*x* :(**¬***R* (*x***)**). (This formula about *x* is satisfiable: it says that *R* is true about *x*, but isn't true about everything.) In
essence, there are two different underlying variables going on, but they each happen to have the same name; from scope it can be decided which one each occurrence refers to. In programming
language terms, we'd say that the inner *x* (the local variable) **shadows** the outer *x* (the enclosing variable). In these terms, free variables in logic
correspond to global variables in programs.

Clearly ∀*x* :(**R****(***x***)**) is always equivalent to
∀*y* :(*R* (*y***)**); variable names are entirely arbitrary (except maybe for their
mnemonic value). So the previous formula might be more clearly re-written as **R****( x)**

**∧∃**

**: (¬**

*y**R*(

*y*)). (This careful re-writing while respecting a variable's scope is called

**α****-renaming**.) Even if 17 quantifiers each used the same variable (name)

**, we could carefully α-renaming 17 times, and end up with an equivalent formula where all quantifiers use distinct variables. This will be useful to avoid potential confusion, especially in the upcoming inference rules (Note, p. 99), where we'll be introducing and eliminating quantifiers.**

*x*Example 4.9

The formula ∀x :(*A* (*x*)) ∧∃*x* :(*B* (*x*)) ∧∀*x* :(*C* (*x*)) is equivalent to the more readable ∀*x* :(*A*
(*x*)) ∧∃*y* :(*B* (*y*)) ∧∀*z* :(*C* (*z*)).

- 2195 reads