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.
