On Saturday, June 15, 2019 at 7:05:57 AM UTC-4, Mario Carneiro wrote: Also the existing definition checker has hardcoded names all over the > place, which has already caused problems on one occasion; adding a $j > parser would fix this issue. >
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. On Fri, Jun 14, 2019 at 1:30 PM Norman Megill wrote: > The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded from >> the current definition check. Any new software will have to treat these 4 >> as special cases, for example by treating them as additional axioms. >> Hopefully these 4 are the only ones that will ever need special treatment. >> > > I would like to renew my suggestion that we change these to ax-bi, > ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an > inconsistent naming convention, since we are signaling that these are > definitions when they don't meet the criteria, and it's also a lie to the > reader because these look like definitions and claim to be definitions and > the user may even know that we check definitions for soundness, yet these > definitions each have extremely subtle problems that make them invalid as > definitions. > I'm pretty sure these meet the literature criteria of being valid definitions. They are eliminable and don't add any new theorems when eliminated down to the primitive language. The class definitions have detailed soundness proofs in the literature. In what sense do you see them as invalid? The problem with calling them axioms is primarily psychological, implying that the real axioms aren't sufficient to express ZFC. It sends the wrong message. Also, they will show up in the "This theorem was proved from axioms" list unless I hard-code them into metamath.exe to exclude them from that list. The issue is that the tools to check them aren't sufficiently sophisticated (and probably will never be) to check that they are valid definitions, so we make them exceptions for the purpose of those tools. (I think an early version of Ghilbert checked the soundness of df-bi using its justification theorem, but I don't recall the details. @raph may wish to comment if he is listening.) As far as I can tell, there will only be these 4 exceptions and no others in the future. Tools could recognize an exceptions list like the mmj2 definition check does now. Or perhaps add a special $j statement? I think you already mentioned that checking tools shouldn't depend on labeling conventions. If the goal is to be open and straightforward, I think it is a more honest > approach to call them axioms and explain in detail why they are > conservative. > But if they are conservative, then they aren't really new axioms. We have very detailed explanations of df-clab, df-cleq, and df-clel on the MPE home page in the Theory of Classes section, and df-bi has a long explanation in its comment. We could enhance the explanations if that would help. > (In fact, df-cleq is not even conservative!) > In the context of ZFC it is, if what you mean is that it depends on ax-ext. That is also explained in the Theory of Classes. And the definition has ax-ext as a hypothesis, so it doesn't actually depend on ax-ext until we eliminate that hypothesis. Norm -- 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/d53fa984-0a88-4681-96a7-42fcb0bb0a5e%40googlegroups.com.
