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(x, y)), the variable 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.
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) x, 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.
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)).