On Sunday, June 16, 2019 at 1:35:04 AM UTC-4, Mario Carneiro wrote: > > > 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. >> > > Metamath is a formal verifier. When it says that something is true, we > believe it because it's checking everything down to the axioms. If we take > that spirit to definitions, it means that when we claim something is > conservative, that should mean that we've checked that it is conservative, > again down to axioms, down to some system that we can check generally for > soundness. So that means that when faced with an unusual definition, we are > faced with a choice: Either we formalize a generic checking process that > can verify the definitional scheme in use, or we assert it as a fact and > leave verification to the meta level, i.e. call it an axiom. >
As presented to the public, Metamath is more than just a formal verifier. It is also an educational tool that presents the ZFC axioms and derives things from them. I think this is an important purpose. For certain technically-minded people who aren't necessarily mathematicians, Metamath has opened up mathematics to them by showing precisely, step by step with very simple rules, how the symbols are manipulated to arrive at results, in a way that they did not fully grasp before. AFAIK there is nothing else that comes even close to doing that. Part of its educational goal is to explain the foundations of mathematics i.e. ZFC set theory to these people. Calling df-clab,cleq,clel "axioms" sends the wrong message, that there's some extra murky stuff that we're not being open about in the beginning and that ZFC isn't sufficient for most of mathematics after all. I think most people who are capable of understanding Metamath proofs can understand how to unwind a class expression by hand and even write a program to do it if they know some computer programming. And I think they can grasp intuitively why class notation is a conservative definitional extension of ZFC and does not really add new axioms. Since you plan to add $j tags to identify the nature of $a statements, can't they be used to indicate that df-cleq, etc. are axioms for your verifier's technical purposes, rather than depend on the hard-coded informal prefixes "ax-" and "df-"? Let the $js indicate what are to be considered axioms by machines and demanding logicians, and let the prefixes indicate how they should be interpreted informally by most people. Another thing that seems wrong is that we would be at the mercy of the sophistication of the definition checking tools, with things possibly changing from ax- to df- over time depending on how the tools evolve. This may send a message that the foundations are unstable and poorly defined. Again, wouldn't $j tags be a more appropriate place for that? We are talking about only 3 or 4 definitions that will never change and never be added to, that are almost universally agreed upon to be valid definitions, that have been justified extensively in the literature. There is zero doubt among mathematicians that they are conservative and eliminable. I don't think it is hard for most technically-minded humans to see that intuitively. In the end, when you get down to the reliability of the transistors in the machine that runs the definition checks, there is no such thing as absolute certainly. At some point common sense is needed to delineate what is acceptable, and to me, the "df-" prefix on these 3 or 4 definitions is an acceptable risk. 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/ad0c4f2f-3dca-4afe-9c72-c48dad853ade%40googlegroups.com.
