|Mathbox for Wolf Lammen||
|Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-section-nf||Structured version Visualization version GIF version|
|Description: The current definition of
'not free', df-nf 1699, has its downsides. In
particular, it often drags axioms ax-10 1966 and ax-12 1983 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 2031).
The mix of both
quantified and simple 𝜑 requires explicit use of sp 1990 (or
in many instances. And, finally, the nesting of the quantifier ∀𝑥
sometimes requires an invocation of theorems like nfa1 2027.
All of this
mandates the use of ax-10 1966 and/or ax-12 1983.
On the other hand, the current definition is structurally better aligned with both the hb* series of theorems and ax-5 1793.
In total, I personally prefer nf2 2090 ∃𝑥𝜑 → ∀𝑥𝜑 (or nf4 2092 ∀𝑥𝜑 ∨ ∀𝑥(¬ 𝜑)) over df-nf 1699. Apart from df-nf 1699, nfi 1705 (but virtually no theorem using them!) I know of no theorem depending on more axioms after switching to nf2 2090 style.
A note on ax-10 1966: 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 nf2 2090 style definition, while use of the current df-nf 1699 incurs these.
A note on ax-12 1983: This axiom enters proofs using Ⅎ via sp 1990 or 19.8a 1988 or their variants. In a context where both mixed quantified and simple variables 𝜑 appear (like 19.21 2036), 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 nf2 2090, but not when using df-nf 1699.
A note on the technique used in this section: I restate nf2 2090 as an axiom instead of defining Ⅎ new. This method allows us to easily determine what axioms a proof depends on (after ignoring the auxiliary axiom) without overloading definitions. Almost all theorems proved in this section correspond to one in the Main part based on the definition df-nf 1699. I will link to it, so a quick comparison on axiom usage is ready at hand.
When checking the definition list in proofs in this section, df-nf 1699 must not occur, as this would create a circular dependency.
(Contributed by Wolf Lammen, 11-Sep-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
|1||wl-section-nf.hyp||1 ⊢ 𝜑|
|Colors of variables: wff setvar class|
|This theorem is referenced by: (None)|
|Copyright terms: Public domain||W3C validator|