Description: Define the not-free
predicate for wffs. This is read "𝑥 is not free
in 𝜑". Not-free means that the
value of 𝑥 cannot affect the
value of 𝜑, e.g., any occurrence of 𝑥 in
𝜑 is
effectively
bound by a "for all" or something that expands to one (such as
"there
exists"). In particular, substitution for a variable not free in a
wff
does not affect its value (sbf 1764). An example of where this is used is
stdpc5 1571. See nf2 1655 for an alternate definition which
does not involve
nested quantifiers on the same variable.
Nonfreeness is a commonly used condition, so it is useful to have a
notation for it. Surprisingly, there is no common formal notation for it,
so here we devise one. Our definition lets us work with the notion of
nonfreeness within the logic itself rather than as a metalogical side
condition.
To be precise, our definition really means "effectively not
free", because
it is slightly less restrictive than the usual textbook definition for
"not free" (which considers syntactic freedom). For example,
𝑥
is
effectively not free in the expression 𝑥 = 𝑥 (even though 𝑥 is
syntactically free in it, so would be considered "free" in the
usual
textbook definition) because the value of 𝑥 in the formula 𝑥 = 𝑥
does not affect the truth of that formula (and thus substitutions will not
change the result), see nfequid 1689. (Contributed by Mario Carneiro,
11-Aug-2016.) |