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 32462
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.)

Ref Expression
wl-section-nf.hyp 𝜑
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