|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
bound by a "for all" or something that expands to one (such as
exists"). In particular, substitution for a variable not free in a
does not affect its value (sbf 1704). An example of where this is used is
stdpc5 1519. See nf2 1601 for an alternate definition which
does not involve
nested quantifiers on the same variable.
Not-free is a commonly used constraint, 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 not-free notion
within the logic itself rather than as a metalogical side condition.
To be precise, our definition really means "effectively not
it is slightly less restrictive than the usual textbook definition for
not-free (which only considers syntactic freedom). For example, 𝑥 is
effectively not free in the bare expression 𝑥 = 𝑥, even though 𝑥
would be considered free in the usual textbook definition, because the
value of 𝑥 in the expression 𝑥 = 𝑥 cannot affect the truth
expression (and thus substitution will not change the result).
(Contributed by Mario Carneiro, 11-Aug-2016.)