On Sunday, June 16, 2019 at 7:35:04 AM UTC+2, Mario Carneiro wrote: > > > BTW if the checker is going to be rewritten, is this a good time to change >> the definition of T. to be A. x x = x <-> A. x x = x? You mentioned that >> there is a special section for df-tru, and it could be eliminated if we >> make this change. >> > > Yes, that would work. >
I understand the advantages of this definition (I used this trick in ~bj-denotes) but I'm not sure this makes for the drawback of introducing syntax belonging to FOL= into propositional calculus (my candidate was ax-tru $a |- T. $.). If you think it's ok, then so be it. But maybe use implication instead of biconditional? i.e. ( A. x x = x -> A. x x = x ). 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/f0b8f0ac-9936-4c93-9525-48ac19a87fbf%40googlegroups.com.
