On Monday, January 27, 2020 at 2:43:37 AM UTC+1, David A. Wheeler wrote:
>
> On Sun, 26 Jan 2020 02:50:31 -0500, Mario Carneiro <[email protected]
> <javascript:>> 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.
>
This corresponds to my yesterday's proposal - to restructure set.mm at a
high level (see
https://groups.google.com/d/msg/metamath/mnkBQV1_cXc/A5OEsTk7AQAJ):
- Volume I. main body of set.mm, consisting of parts 1-17
- Volume II. supplementary material, consisting of parts/chapters like
"Set Theory according to Bourbaki" (Benoit's hobbyhorse) or "Algebraic
Structures according to Bourbaki" (my hobbyhorse), etc.
- Volume III. mathboxes (current part 21)
- Volume IV. alternative definitions and theorems: the current parts
18-20 could be placed here, but also a part/chapter containing David's
definitions and theorems for ">".
So my "Volume IV." corresponds to David's section "Other definitions". But
maybe it is sufficient to have an area between the current main body of
set.mm and the mathboxes (Volume II.). To mark definitions and theorems for
e.g. ">" should be sufficient to prevent that these are used arbitrarily,
but they could be used in the mathboxes if somebody wants to experiment
with them.
Hence, the following could be (an example for) a substructure of Volume II.:
- Immature definitions and theorems
- "Set Theory according to Bourbaki"
- "Algebraic Structures according to Bourbaki"
- ...
- Deprecated definitions and theorems
- (PART 18) ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS
(DEPRECATED) - if not deleted completely meanwhile...
- (PART 19) COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)
- (PART 20) COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
- Alternative definitions and theorems
- Greater than (">") and greater than or equal to (">_").
To have only one additional "Volume" instead of two may respect the
concerns of vvs (see
https://groups.google.com/d/msg/metamath/mnkBQV1_cXc/Xkrv9_9AAQAJ) a little
bit...
--
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/d052dad3-f0a1-4ac4-ace7-3989253756f8%40googlegroups.com.
