> Could you elaborate on this? I would assume that once you have nfi and nfri you can easily convert between the two styles.
The conversion ist still possible. But nfi uses both ax-10 and ax-12, sth that I'd like to avoid if possible. This in some cases inevitably lead to different proofs for both versions. Wolf [email protected] schrieb am Sonntag, 12. September 2021 um 16:03:44 UTC+2: > > (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/03fca508-b1e4-407c-a134-93382115f8d2n%40googlegroups.com.
