I deleted this conversation, because of awful formatting. For some unknown reason, I was not allowed (or able) to edit my text. In the end, I deleted the one you posted to, and opened a new one with improved style. If possible, please react to the updated conversation.
ookami schrieb am Sonntag, 12. September 2021 um 16:21:02 UTC+2: > > 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/f6837baa-ba5e-46a0-bb46-915b0b787ab8n%40googlegroups.com.
