First-Order Logic: bound variables, free variables 1.7 2004/07/01 12:51:23 GMT-5 2009/01/09 10:42:09.049 US/Central Ian Barland ibarland@radford.edu John Greiner greiner@cs.rice.edu Phokion Kolaitis kolaitis@cse.ucsc.edu Matthias Felleisen matthias@ccs.neu.edu Moshe Vardi vardi@cs.rice.edu Ian Barland ibarland@radford.edu John Greiner greiner@cs.rice.edu Fuching Chi iamjack@rice.edu B . c@rice.edu Bryan Cash seleniat@rice.edu Sarah Elizabeth Trowbridge set@rice.edu 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. The concept “x free in φ” 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 Rx 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 occurence 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 Rx 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, 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 .