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 ) ) > > 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/ce1510da-d521-4bbc-bfe5-1dc96ec80826%40googlegroups.com.
