On Sun, 26 Jan 2020 02:50:31 -0500, Mario Carneiro <[email protected]> wrote: > 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. ... > I can't properly appraise > the appropriateness of a definition without seeing how it is going to be used.
We seem to talking past each other. I *agree* with you & Norm that if a definition is going to be used, we should focus on ensuring there are a number of theorems that will use it, and show that the definitions are useful before accepting it. A definition intended for use needs to earn its keep. That is *not* what I'm talking about. I'm not talking about creating definitions intended for use in later proofs. I'm talking about definitions created *specifically* to *not* use them, but instead to define them so that people will know what *other* materials & set.mm comments mean by those expressions. For example, these definitions can serve as a kind of Rosetta stone to explain others' notations, as well as formalizing the use of such terms in set.mm comments. For example, a lot of set.mm comments refer to "greater than", but we do not formally define the expression. That concept should be defined as rigorously as we can reasonably do it. David A. Wheeler: > > 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. Mario: > 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. Yes. That's not my *primary* motivation, but it's a good side-effect. > 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.) That's easy: Add a new section to set.mm at the end, *after* the mathboxes. Call it "Other definitions" or some such. All definitions there are discouraged. We'd want a few theorems to show that each of the definitions have the "expected" behavior, but there'd be no need to create all the "support" theorems that make such definitions easy to use. Then the tools will ensure that those definitions can't be used by anything else, since they're at the end & would be marked to discourage further use. But they *can* be discovered, typeset, referred to if someone wants to know what a term in a comment means, etc. If it turns out they're more useful than originally expected, they can be moved up per our usual process. I'll try to mock up in my mathbox what I have in mind. I really already have a starting point with ">" and the hyperbolic functions. --- 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/E1ivtR9-00020Q-Td%40rmmprod07.runbox.
