Given Norm's preferences, I will put my vote in for F/4. It's not very intuitionistically satisfying, but that's a problem for another database. (I would use F/2 in iset.mm.)
On Tue, May 28, 2019 at 6:28 PM Norman Megill <[email protected]> wrote: > On Tuesday, May 28, 2019 at 12:10:24 PM UTC-4, Benoit wrote: >> >> On Tuesday, May 28, 2019 at 6:02:38 PM UTC+2, Mario Carneiro wrote: >>> >>> 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 ) ) >>> >> > I think my preference for the official definition would be F/2 or F/4, > then F/1, then F/3. F/1 (our current definition) has the slight inelegance > of nested quantification, and F/3 is somewhat non-intuitive (to me). > > If you want to replace our official df-nf with F/2 or F/4, that's OK with > me. I'm not bothered by the use of df-ex but F/4 seems the "most" > intuitive to me. > > Norm > > >> >>> 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. >>> >>> >> Thanks Mario. The form F/4 is already there as bj-nf3; the form F/3 is >> interesting and I will add it, together with your remarks on comparative >> advantages. >> > -- > 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/522281b2-d851-44fe-9e29-20fd2428e498%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/522281b2-d851-44fe-9e29-20fd2428e498%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/CAFXXJSvGhhF3hYWC0VTO6xob8R5Ym6Obxo18B%2BwYDsGrtC%3DMvg%40mail.gmail.com.
