Hi all, I wanted to draw attention to Wolf Lammen's recent work in the "existential uniqueness" section. His proof of mo2v (compare it with mo2) removed dependency on ax-11 and ax-13 from moim, mo2icl, and several other theorems depending on them.
This was made possible by his new proof of eu5 (compare eu5OLD), that removes dependency on ax-7,10,11,12,13 from eu5 and several theorems depending on it, including eumo. (Also note that the new proof of eu5 uses no dummy variable; actually, it only uses euex and propositional calculus.) Probably the same thing can be done by proving some other "dv-versions" of existing theorems: mov, mo3v, eu1v, eu2v, eu3v, sb8euv, eumo0v (after checking that each "nf-version" indeed requires the additional axioms). Similarly, proving mo4 directly (and not from mo4f) should remove some dependencies as well, including from eu4 (and maybe they could be relabelled mo4 / mo4v to follow the same pattern, at least in this section --- the pattern xxxf / xxx coexists in other sections). Indeed, there is a common pattern that the use of a non-freeness $e-hypothesis instead of a dv-condition requires ax-11 (typically from nfal) and ax-13 (typically from hbs1). Wolf has certainly already seen that, but I wanted to give it more publicity by posting it on the discussion group. I also think that in this case, both the "nf-version" and the "dv-version" can coexist in the main part of set.mm, given that they are in a relatively early part of set.mm, that each have their use, that the nf-version is slightly more general, and that the dv-version requires fewer axioms. Two remarks: * I think that some dependencies on ax-12 can be removed (as well as some dependencies on ax-10) by adopting an alternate definition of non-freeness, see df-bj-nf and its comment, and compare bj-nfn with nfn. * With the same goal as Wolf, I recently added vtoclg1f in order to remove dependency on ax-11 and ax-13 from the important vtoclg and several theorems depending on it (including sbc8g). I'll be interested in your comments, especially on adopting the alternate definition for non-freeness. Benoit -- 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/25b494de-7940-4876-b474-a9421c379d44%40googlegroups.com.
