> (a) There is more friction in the transition between hb* and nf* style theorems
Could you elaborate on this? I would assume that once you have nfi and nfri you can easily convert between the two styles. On Sun, Sep 12, 2021 at 9:16 AM 'ookami' via Metamath < [email protected]> wrote: > 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. (a) There is more > friction in the transition between hb* and nf* style theorems; (b) 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/65eeae41-40f2-40dd-9f36-2b8847c8b498n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/65eeae41-40f2-40dd-9f36-2b8847c8b498n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSuPXYD9QNCa77HNcgOtK1u%2BVOZQc1fek%2B0B9kjvXtsXLA%40mail.gmail.com.
