| Description: The current definition of
'not free', nf5 2102, has its downsides. In
particular, it often drags axioms ax-10 2006 and ax-12 2034 into proofs, that
are not needed otherwise. This is because of the particular structure
of the term ∀𝑥(𝜑 → ∀𝑥𝜑). It does not allow an easy
transition 𝜑--> ¬ 𝜑 (see nfn 1768).
The mix of both
quantified and simple 𝜑 requires explicit use of sp 2041 (or
ax-12 2034)
in many instances. And, finally, the nesting of the quantifier ∀𝑥
sometimes requires an invocation of theorems like nfa1 2015.
All of this
mandates the use of ax-10 2006 and/or ax-12 2034.
On the other hand, the current definition is structurally better aligned
with both the hb* series of theorems and ax-5 1827.
A note on ax-10 2006: The obvious content of this axiom is, that
the
¬ operator does not change the not-free
state of a set varable.
This is in fact only one aspect of this axiom. The other one, more
hidden, states that 𝑥 is not free in ∀𝑥𝜑. A simple
transformation renders this axiom as (∃𝑥∀𝑥𝜑 → ∀𝑥𝜑),
from which the second aspect is better deduced. Both aspects are not
needed in simple applications of the df-nf 1701 style definition, while use
of the current nf5 2102 incurs these.
A note on ax-12 2034: This axiom enters proofs using Ⅎ via sp 2041 or
19.8a 2039 or their variants. In a context where both
mixed quantified and
simple variables 𝜑 appear (like 19.21 2062), this axiom is almost
always required, no matter how 'not free' is defined. But in a context,
where a variable 𝜑 appears only quantified, chances
are, this axiom
can be evaded when using df-nf 1701, but not when using nf5 2102.
(Contributed by Wolf Lammen, 11-Sep-2021.) (New usage is discouraged.)
(Proof modification is discouraged.) |
