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/a629e5a4-306e-4c9c-9fe9-f0542ceb3956n%40googlegroups.com.
