On Fri, 24 Jan 2020 19:29:17 -0800 (PST), Norman Megill <[email protected]> wrote: > My essay yesterday represents the opinion I formed after looking back and > reflecting on some things I felt were accomplished successfully and others > not so successfully with set.mm. I try to keep an open mind, and my > opinion can change if I can be convinced another way is better.
Norman Megill, 2020-01-23 point 1: > There is no "goal" per se for set.mm. > People work on what they are interested in. I think that's a necessary side effect of working with many people. People will have different goals, and where we *can* find ways to work together it's great to do so. In general I think the results are stronger for it when we can make that happen. Norman Megill, 2020-01-23 point 2: >A very important thing to me is the philosophy of striving for > simplicity wherever possible. This particularly impacts what definitions > we choose. For me, simplicity is not a goal in itself, but it *is* necessary to support other goals. My real goal is having strong formal proofs of the majority of significant mathematical claims, recorded in a way that it can be archived for the future. Relative simplicity is a necessary part of that. I think you can go too far in some notions of simplicity. For example, I appreciate MM0's ability to add arbitrary parentheses (not available in straight Metamath). But those are not critical, and there is so much to appreciate about Metamath. So let's talk about definitions in set.mm, which is really a question about how to best create certain Metamath databases. After all, all agree that the Metamath language & toolsets support adding definitions. Having many definitions has problems as noted: > Definitions are at the heart of achieving simplicity. While developing > set.mm, two rules of thumb that evolved in my own work were (1) there > shouldn't be two definitions that mean almost the same thing and (2) > definitions shouldn't be introduced unless there is an actual need in the > work at hand. Maybe I should add (3), don't formally define something that > doesn't help proofs and can be stated simply in English in a theorem's > comment. There are good reasons to do this. For example, with multiple similar definitions: > It was a constant nuisance to have to convert back and forth i> nside of proofs, making proofs longer. I eventually decided to use just > "e." and "C_", and it made formalizations much more pleasant with fewer > theorems and shorter proofs... Some may expect me to disagree with this. But no, I strongly agree with Norm on this point. Every time there's a set of similar definitions in wide *use* in set.mm, there's a risk of having to do a lot of back-and-forth conversions. Having conventions prefer one form over another simplifies proofs and reduces the number of necessary theorems. > *4.* As for adding an exhaustive list of all possible definitions one can > find in Bourbaki or whatever, as someone suggested, I don't think something > like that belongs in set.mm, for all the reasons above. There are other > resources that already list these (Wikipedia, Planetmath, nLab). Their > precise formalization will depend on the context in which they are needed > in set.mm, which is unknown until they are used. In isolation (perhaps > with a couple of property theorems that basically check syntax) there is no > guarantee that they are correct, even in set.mm. To restate, I think the > philosophy should be that definitions should be added by need, not as > busywork. >Adding a definition when needed is one of the smallest parts of > building a series of significant proofs. It doesn't have to be done in > advance, and I don't think it is generally productive or useful to do so. I think we should not try to create an "exhaustive list of definitions". I have not proposed such a thing. But I *do* think that we *should* provide over time a set of standardized "definitions with significant use in mathematics" along with a relevant expression in set.mm (and iset.mm). This reflects a difference in our goals. My goal is not simplicity for its own sake. My goal is to formalize all significant mathematical works so that they are far more certain & can be archived for all future time. >From that point of view, failing to formalize commonly-used terms such as "<" is just that: a *failure*. And it's an unnecessary failure. Adding definitions of common terms is one of the smallest parts of building a set of significant proofs. Thus, defining these terms is one of the most *productive* things that can be done to formalize common mathematics, *because* it takes less time than some other activities to produce results. I don't accept that "There are other resources that already list these". Most of them do not formalize definitions to the same degree as set.mm, and there's no guarantee that their terminology matches set.mm even when they are formal. In addition, I think it's unwise to assume that these resources will necessarily exist the future. Almost all of Stoic logic is lost forever, even though that was the primary system of logic for centuries. We've lost about 2/3rds of Aristotle's works, and people *tried* to keep them. More recent works are much *more* likely to be lost, since recording devices only last ~10years and copyright laws often make archiving illegal. Closer to home: Many old Metamath discussions that have been lost forever due to one of the old websites suddenly imploding. While set.mm *should* give credit to all external resources, we should not assume that those external resources will always exist. In the long term it is unlikely that everything we reference will be available. It will be much easier to archive set.mm than other sources, *because* it can provide a single uniform archive. That would be fantastic. > IMO the same should be done with >, mentioning what it means in the > description for <. Introducing a formal $a statement for > that will never > be used is unnecessary and wasteful of resources. No, I don't agree at all, because this depends on what your goals are. If your goal is to record all major mathematical constructs, then recording ">" is absolutely necessary. > If we want to be > excessively pedantic, we could mention in the description for < that the > the formal definition would be "|- > = `' >" , although that seems less > intuitive than simply saying that "in theorem descriptions, we occasionally > use the terminology 'A is greater than B' to mean 'B is less than A'." No, that would be useless. Because it's in a comment, it would *not* go through formal checks, and we couldn't prove a few simple theorems to show it works as intended (e.g., "4 > 3"). So including that information in a comment is *much* worse than using $a. Now, regarding: > wasteful of resources. I think what I have in mind is *not* a waste of resources. I also think there's a potential misunderstanding here. Perhaps a clarification will help. I *agree* that set.mm should *not* try to *use* definitions like ">" in arbitrary ways. As noted above, that leads to much longer & more complex proofs (because the proofs have to do many conversions), as well as a huge number of theorems necessary to support the use of such definitions. For example, to seriously *use* ">" you can't just create the definition, you have to create a lot of supporting theorems to support its convenient use. I do *not* advocate adding definitions like ">" to be used in this way, for all the reasons listed above. So I *agree* with your concerns, and I think we can do something else that will avoid those problems. What I'm advocating for is a section near the end of set.mm, let's call it "Other definitions", where definitions of other commonly-used mathematical constructs are formally defined *and* are expressly marked as "(New usage is discouraged.)". The purpose of this section would *not* be to create definitions for use (that would be expressly discouraged!). The purpose of the section would be to formally define and record, for future readers, the meaning of other common mathematical constructs using set.mm concepts. It would also help people understand what constructs they *should* use by convention - they can look up what they planned to use, and see what is recommended instead. Think of it as a Rosetta Stone. This would have practically no resource use. Each construct would have a definition, plus maybe 1-3 other theorems (e.g., to express it more clearly, relate it to other expressions that would be used in set.mm instead by convention, or to demonstrate that it has the "expected meaning"). This would be vanishingly small subset of the definitions and theorems in the rest of it (especially as it starts approaching "all of mathematics"). Please note that this would *not* have the problems noted earlier. There would be no "converting back and forth" in normal proofs, because these definitions would be expressly marked as symbols not to be used in the normal case. You wouldn't normally see these other constructs in formal statements unless you were looking for them. It *would* make it easier to use these other symbols in comments, because they *would* be defined, and now those symbols would have "real" definitions if someone wanted to learn exactly what was intended. Anyway, I hope this helps clarify the difference. I'm hoping to talk you eventually into letting me add that new section :-). --- David A. Wheeler -- 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/E1ivU9j-00032f-FB%40rmmprod07.runbox.
