I was asked somewhere else to elaborate more on > There is more friction in the transition between hb* and nf* style theorem;
Yes, it is still technically possible to convert from hb* to nf* via nfi. But nfi, proved from nf2, depends both on ax-10 and ax-12 (see wl-nfi <file:///home/wolf/metamath/web/wl-nfi.html>). Such a use counteracts our goal of minimizing axiom usage. Hence, in some cases, different proofs for both versions are inevitable. One such example is nfth <file:///home/wolf/metamath/web/nfth.html>. We cannot base its proof on nfi, but instead have to replay the proof replacing ph with E. x ph in an a1i <file:///home/wolf/metamath/web/a1i.html> step. This is demonstrated in wl-nfth, already available on github, but not yet on the web site. Wolf ookami schrieb am Sonntag, 12. September 2021 um 15:24:56 UTC+2: > Hi, > > I recently uploaded a couple of theorems to my Mathbox, starting with > http://us2.metamath.org:88/mpeuni/wl-section-nf.htm, that demonstrate how > things could have developed, if one had picked > http://us2.metamath.org:88/mpeuni/nf2.html instead of > http://us2.metamath.org:88/mpeuni/df-nf.html as the defining term for > 'Not Free (Ⅎ)'. > > > The results show, that one can expect in predicate logic an overall > reduction of the usage of http://us2.metamath.org:88/mpeuni/ax-10.html, > and perhaps a marginal decrease in use of > http://us2.metamath.org:88/mpeuni/ax-12.html. > > > This certainly positive result is due to the more symmetric structure of > nf2 wrt to negation, and the avoidance of mixed quantified and not > quantified variables. But it comes with a price, too: > > - There is more friction in the transition between hb* and nf* style > theorems; > - Axioms like ax-5 need the old style for full exploitation, so there > is a sort of disruption in technique present. > > You will find more details in a > http://us2.metamath.org:88/mpeuni/wl-section-nf.html. > But these are my thoughts. Let me hear how you think about a change of > definition of 'Not Free'. > > > Wolf Lammen > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4247f79e-1f55-4845-b9bd-74926f07db5bn%40googlegroups.com.
