On Tue, Jun 18, 2019 at 10:19 PM Norman Megill <[email protected]> wrote:
> 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 totally agree on the usefulness of Metamath as an educational tool. But I also want to be sure that our actions match our words to the degree possible. I think that students who are interested in Metamath have already had enough of "white lies" about foundations, and are trying to dig to the heart of it. If ZFC is supposed to be enough, then let's build exclusively on ZFC. If there are pragmatic problems with that, then explain those problems as you add an axiom to that effect. > 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. > I think that's not a bad idea. You are right that if we have an alternate means of signaling to the computer, then we can let the name be what it's supposed to be - a mnemonic that assists in understanding the shape and role of the statement in context. > 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? > One thing I should probably have said more explicitly is that a definitional schema is nothing more or less than an axiom schema (of a variety more complicated than the things metamath usually calls schema). Replacing a single axiom with an extension to the definition checker is basically trading one axiom for a whole bunch of axioms, and usually the latter will be much more complicated to verify. So for one-off "definition-like" axioms, it's probably not worth building a complicated axiom schema. Just like with theorems in set.mm, we want to know that a theorem "pays for itself" in terms of use. Most of the definitional schema implemented in mmj2 pays for itself, because it supports a large variety of definitions that stress most of the features. The justification theorem extension does not pay for itself, because it is only being used for df-tru (and I am also calling the extension itself into question). And all of the definitional extensions I proposed in the previous email would not currently pay for themselves, because there is only one or two uses of each of them. It's possible that in the future they will get more use, but I think the better practice is to build the unifying framework only after several examples already exist. So while I think it is possible to extend more things into the definitional schema, it's much more light-weight to just have a few axioms instead, and judge them on a case by case basis. And what of "conservativity"? My focus here has been on axioms that are "correct", i.e. true in any model of ZFC for an appropriate interpretation of all the "defined" symbols. This is actually sufficient to ensure conservativity over ZFC, since any axiom that is true in every model of ZFC is provable in ZFC and hence is conservative over it. So I am absolutely okay with $a |- T. because it's trivial to verify in a model of ZFC and it's also intuitively correct. There is no need for this to be an eliminable symbol or anything like that, although it's nice when we can obtain 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. > How about adding some weasel words to the affected definitions? Such as: "This definition is technically an axiom, in that it does not satisfy the requirements for the definition checker. The proof of conservativity requires external justification that is beyond the scope of the set.mm axiomatization." -- 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/CAFXXJSsmQLg2PxWLUaTpOwabGF2iN2d%2B4_AtT4XU_32bHqBJsQ%40mail.gmail.com.
