I'm okay with the alternative df-bj-nf definition. If the use of the definition E. is undesirable, here are some more alternatives:
$a |- ( F/1 x ph <-> A. x ( ph -> A. x ph ) ) $a |- ( F/2 x ph <-> ( E. x ph -> A. x ph ) ) $a |- ( F/3 x ph <-> ( -. A. x ph -> A. x -. ph ) ) $a |- ( F/4 x ph <-> ( A. x ph \/ A. x -. ph ) ) F/1 is the original definition, F/2 is Benoit's. F/3 and F/4 are equivalent to F/2 up to df-ex and propositional logic. F/3 has the advantage that it uses only primitive symbols, and appears as a commutation. F/4 has fewer negations and is easy to understand in terms of ph being always true or always false. And F/2 has no negations and uses the dual quantifier instead. On Tue, May 28, 2019 at 11:47 AM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/25b494de-7940-4876-b474-a9421c379d44%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/CAFXXJSu3QCWYYtGcag84CVtzMx33nNym9GRu3rj%2B7XRcryvSvw%40mail.gmail.com.
