I want to try to draw some conclusions from (or to express just my
impressions of) the discussion until now:
Differentiation between long-term goals and short/mid-term goals
Whereas the long-term goals semm to be clear and acceptable for everybody
(to have a knowledge base containing *all* known mathematics formalized),
there are different opinions about the short/mid-term goals: how shall we
continue working on set.mm?. Therefore, this discussion should concentrate
on these short/mid-term goals.
Different "levels" of (short/mid-term) goals
It seems that there are different "levels" of (short/mid-term) goals:
- level 1 - general goals: These goals are universal for (the main body
of) set.mm itself and all users of set.mm. They should be expressed as part
of the "Conventions" . We may need also two levels of conventions: overall
conventions valid for the whole set.mm, and conventions to achieve the 1st
level goals. Anybody not agreeing with the overall conventions (at least in
some extend) should not use set.mm, but should create a separate database
to achieve his/her goals. The conventions for the 1st level goals contain
the criteria for moving definitions/theorems into the main body of set.mm.
By this, the conventions can be regarded as analogue to the "Universal
Declaration of Human Rights" or to the "Ten Commandments" in the bible
(this comparison is extremely exaggerated, I know).
To describe such 1st level goals, we can assign the following
ascertainments to purposes and properties of set.mm:
- Purpose: knowledge base, which also can be used as library and for
teaching/research
- Completeness: should cover most important theorems of mathematics
(Attention: this must be clarified/specified in more detail, because this
seems to be the main reason for the current discussion...)
- Beauty, Simplicity: Here we should give (and have already) some
precedence rules, e.g. "shorter proofs are prefered", or "proofs using
less
axioms are prefered",...
- Rigor: currently assured, but must be kept whatever happens
- level 2 - common goals: These are goals shared by a group of users who
want to work collectively on reaching these goals. This was expressed in
several posts that several users could have a different opinion on what is
"beautiful", "an elegent proof", "a good structure", a "useful theorem",
etc.
- level 3 - personal goals: as long as these goals do not contradict the
overall conventions, they could be whatever the user wants.
High level restructuring of set.mm
Although it is clear that the main body of set.mm should serve the general
goals, it is yet not clear how to handle 2nd level goals. A proposal (which
was given in several ways by several people) could be to restructure set.mm
at a high level: currently we have two "parts"/realms of set.mm ("part" not
in the meaning as it is currently used in set.mm - maybe the currently used
"parts" should become "chapters"...):
- main "part"/body of set.mm
- mathboxes
Since it is clear where the 3rd level goals belong to (to the mathboxes!),
it is not clear where to work on the 2nd level goals (and this is the main
reason for the current discussion). For some users it is not sufficient to
work on them in the mathboxes, and for other users it is not
acceptable that these are contained in the main body of set.mm. To be
specific, I would propose the following structure (the titles can/should be
discussed):
- 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 ">".
Definitions/theorems contained in Volume IV. need not to be marked as
"usage discouraged", because they cannot be used in proofs of Volumes
I.-III., but it should be possible to use them within Volume IV. without
restriction. By the way, the ALT-definitions/theorems currently contained
in the main body may also be moved into this Volume IV.
Could this be an approach to find an acceptable way to achieve everybody`s
short/mid-term goals? What would remain to be discussed are the criteria
for definitions (and/or theorems) serving the 1st level goals, i.e. which
definitions are acceptable to be added to the main body/Volume I. of
set.mm...
--
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/40321bdd-8217-4450-ae6b-77bb78d533a4%40googlegroups.com.
