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 2368). An example of where this is used is
stdpc5 2063. See nf5 2102 for an alternate definition which
involves 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
free," because
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 𝑥 = 𝑥 (see nfequid 1927),
even though 𝑥 would be considered free in the usual
textbook
definition, because the value of 𝑥 in the expression 𝑥 = 𝑥 cannot
affect the truth of the expression (and thus substitution will not change
the result).
This definition of not-free tightly ties to the quantifier ∀𝑥. At
this state (no axioms restricting quantifiers yet) 'non-free' appears
quite arbitrary. Its intended semantics expresses single-valuedness
(constness) across a parameter, but is only evolved as much as later
axioms assign properties to quantifiers. It seems the definition here is
best suited in situations, where axioms are only partially in effect. In
particular, this definition more easily carries over to other logic models
with weaker axiomization.
This predicate only applies to wffs. See df-nfc 2740 for a not-free
predicate for class variables. (Contributed by Mario Carneiro,
24-Sep-2016.) Converted to definition. (Revised by BJ,
6-May-2019.) |