Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-section-nf Structured version   Visualization version   GIF version

Theorem wl-section-nf 32294
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 ax-12 1983) 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.)

Hypothesis
Ref Expression
wl-section-nf.hyp 𝜑
Assertion
Ref Expression
wl-section-nf 𝜑

Proof of Theorem wl-section-nf
StepHypRef Expression
1 wl-section-nf.hyp 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator