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 xx is bound if it is in the body of
a quantifier ∀ x∀x … or ∃ x∃x ….
Otherwise, the occurrence is free.
For example, in
∀x.
likes(x,y)∀x.likes(x,y)
,
the variable yy is free but xx is not.
So this is a statement about yy;
we can't evaluate this to true/false until we get
some context for yy.
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.∀x.,
so xx really is bound.”
(Just as 7 is prime, even though people sometimes use 7 in the context
of 7+1.)
Whether xx is free in a φφ can be determined by a function
isFreexφ
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)
)(R(x)∧∃x.
¬R(x)
).
(This formula about xx is satisfiable:
it says that RR is true about xx,
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 xx (the local variable)
shadows the outer xx (the enclosing variable).
In these terms, free variables in logic
correspond to global variables in programs.
Clearly
∀x. R(x)∀x.R(x)
is always equivalent to
∀y. R(y)∀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)
)(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) xx,
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)
)(∀x.
A(x)
∧∃x.
B(x)
∧∀x.
C(x)
)
is equivalent to the more readable
(∀x.
A(x)
∧∃y.
B(y)
∧∀z.
C(z)
)(∀x.
A(x)
∧∃y.
B(y)
∧∀z.
C(z)
).
