On Sat, Jan 25, 2020 at 11:36 PM David A. Wheeler <[email protected]> wrote:
> On Sat, 25 Jan 2020 18:40:53 -0800 (PST), Norman Megill <[email protected]> > wrote: > > I know I keep harping on not wanting to add a catalog of definitions > (with > > shallow theorems) that are otherwise unused, but it has been done in the > > past with the work essentially wasted, sometimes causing resentment, and > I > > want to avoid that. With an ambitious goal like "all of mathematics," > it > > will be very tempting to start collecting definitions, leading to a > false > > sense of accomplishment to see the syntax errors ironed out and simple > > property theorems proved. > > Not just tempting. Necessary. > I think I would also advocate a "theorems first" approach here. Assuming that mathematicians have done their work right, definitions should naturally fall out of the commonalities between theorems that are stated in the literature. We don't need to give them any help in this - good definitions make themselves known. After writing the same sequence of characters enough times you get tired and want to compact it to something more manageable. I think the point about wasted work causing resentment also requires acknowledgement. I would give at least a 50% chance, maybe more, that an untested definition will need to be rewritten when one really gets around to using it, and attribution at this point becomes messy, because the original author may feel slighted by a rewrite (they shouldn't, set.mm is public domain and we have always recognized that your theorems may be rewritten to suit future work, but sometimes we get attached to things anyway). While I don't really want to enforce a policy along these lines, I certainly place the worth of untested definitions very low. They can be recreated on first use with little trouble. > But in the end it is busywork with a good chance > > of being discarded later. Moreover, a few shallow value and property > > theorems don't ensure that the definition is correct, possibly > misleading > > someone who might want to use set.mm as a reference source that can be > > trusted to be rigorously correct. > > *Nothing* other than human review ensures a definition is correct. > If we defined 9 as "( 8 + 3 )" there is no tool that could detect the > error. > Tools can detect if a definition is syntactically valid, > but no tool can figure out "was this really what you meant?" > I disagree with this sentiment. If you define 9 to be 8 + 3, then you will later stumble when trying to prove that 9 * 9 is 81, or 9 + 1 = 10, or 9 is the first odd composite greater than 1. Basically, proving theorems about a definition boxes it in, making it much less likely that you got the statement wrong if all the expected proofs go through. If the only proof you do is the definitional theorem, you only get a very weak version of this, because the definitional theorem is much more likely to be correlated with the definition itself, so it is quite possible for errors to make it past both the axiom and the definitional theorem. The best solution for that is to provide definitions & enable multi-person > human review to *detect* those problems. Failing to formalize those > definitions means that the needed multi-person review can't ever happen. > If it isn't in set.mm, it doesn't need to be reviewed. Review only happens *after* some development is submitted. And again, I can't properly appraise the appropriateness of a definition without seeing how it is going to be used. A useful additional step would be to prove some "expected" properties to > ensure that they "do what's expected". Again, that requires that they > be formalized in the database itself somewhere. > If you are talking about "unit tests" like 9 + 3 = 12, that's good, but it is no substitute for general theorems, which constrain the definition in a much broader way. > This is the motivation for rule 2 I > > proposed, "definitions shouldn't be introduced unless there is an actual > > need in the work at hand." > > I would add: > ... or if the definition will *never* be used by the rest of set.mm, and > it is > there solely to help translate widely-used constructs used in the > literature. > I can actually see a use for this, in the sense that having a definition in main blocks future attempts to add that definition. If we have a definition for greater-than, then we won't get repeated requests to add it because it's already there. At the same time, that's a bunch of unnecessary axioms to add to the database, and we would have to guard them against use, which sounds like extra complexity for the review process. (Yes I know we have discouraged theorems, but it's still something we have to monitor.) 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/CAFXXJSsAZNLFTEWnFL1knc7qt4vAL-8sO0NWBWnU3JgCfEd-bw%40mail.gmail.com.
