On Sun, Jun 16, 2019 at 8:08 PM Benoit <[email protected]> wrote:
> 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 ). > I'm also okay with making it an axiom - as I've said, I think axioms have their place and minimizing axioms isn't necessarily the best idea anyway. My impression has been that people prefer straightforward interpretations over fewer axioms. Things like ax-meredith are an interesting observation but no one actually builds logical systems on them, and the laws of boolean algebra are another example - everyone knows the list of axioms is redundant in a few places but it's easier to explain if we don't try to minimize things and break symmetry. I believe Norm's argument is that this suggests that ax-1,2,3,mp are not complete for propositional logic, but I think that's actually true if you use the metamath interpretation of "complete" as metalogically complete, because you can't get propositional constants without it. Anyway this is rehashing arguments in another thread so I'll leave it here. As for replacing <-> with ->, I agree. Implication is a primitive constructor, and id is proven before biid, so this makes the definition simpler in both the definition itself and the proof of tru. There are shorter proofs than id, but none proves a shorter statement. (In fact, id is the shortest tautology in prop calc using only primitive constructors.) Mario -- 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/CAFXXJSvoS_HWMmgfuhOYBZBjAi1LhV_VRsW3G0nNsd13M6PwXA%40mail.gmail.com.
