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. > 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?" 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. 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. > 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. BTW, a possible place for my proposed "Other definitions" section would be *after* all the mathboxes. That way it'd be impossible for someone to accidentally use those definitions within a mathbox. That could also make it crystal-clear that these definitions are not for use within the regular database, but are instead provided to ensure that there are definitions for the *other* widely-used terms conventionally avoided in set.mm. --- 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/E1ivZf1-0002ZS-6x%40rmmprod07.runbox.
