Hi all, Here is my take on the "goals and philosophy" for set.mm:
Overall, I'm also seeing the end goal as set.mm covering "all of mathematics", which means I would not exclude any theorem. *As for the audience*, I think the goal shall be that any interested person, with even limited background, can grasp our definitions. So, they shall be as simple as possible, and rely on basic concepts whenever possible. That does not prevent us to provide an definitions or equivalents, relying on more advanced or less-used concepts. *About which theorems shall enter the main part of set.mm*, I think Norm and Mario's philosophy of "based on need" is good. To give a concrete example, when I wanted to prove general things about probability theory, with the help of people on the mailing list, I found out I needed to define the Bochner integral, which required to define the canonical homomorphism from the real numbers `RRHom`, which in turn required extension by continuity `CnExt`, and uniform structures `UnifSt` and `metUnif`, in turn requiring pseudometrics `PsMet`. So, I ended up adding pseudo-metrics to set.mm, not in order to be exhaustive, but because I had a practical end-goal for that. I have not yet come back to the Bochner integral, but there are several interesting theorems about extension by continuity I'm happy I added, and which will probably be useful for other things. Just like for groups, there are other generalizations of metrics than pseudometrics (quasi-, meta-, semi-, pre-, etc.), I introduced only pseudometrics, and for a good reason. When introducing the concept of pseudometric, I did not change the definition of metric so that metric is seen as a specialization of pseudometrics, but kept the generic definition, and just added the generalization theorem ~xmetpsmet. *More generally about new definitions*, I also think interesting definitions are those which summarize complex concepts into a simpler form. In the example given by Norm, ` A C_ B ` stands for ` ( A i^i B ) = A ` (~df-ss) or ` A. x ( x e. A -> x e. B ) ` (~dfss2). The form ` A C_ B ` is shorter and more convenient than both, and is widely used. In ` A > B <-> B < A `, the new form "greater than" is exactly as long and as convenient as ` A < B `, I see no added value to /use/ it. It may still be interesting to /define/ it, just to express "how it would look like if we had to define this concept in set.mm", but I believe we shall explain in the comments why we don't use it in set.mm, and refer to the "less than" definition. Another example which comes to my mind is "countable". I have a few theorems about countable sets in my mathbox <http://us2.metamath.org/mpeuni/mmtheorems273.html#mm27298s>. We could imagine to define the class of countable sets, like `Count = { x | x ~<_ _om }`. However, stating that a set is countable using `A e. Count` would be just as long and convenient as stating `A ~<_ _om`. I think this is another good example where we don't need to introduce a new definition, although, it may not be obvious at first (it was not to me), that `A ~<_ _om` means `A is countable`, because none of the concepts there (dominance relation, natural numbers), are simple concepts. *Concerning the structure of set.mm*, while I like the idea to add definitions in a specific sections, I'm afraid that this would break its overall structure, we could consider another option, where "other concepts" not developed in set.mm would still be in the corresponding chapter (like, putting magmas in the algebra section, just defined, not developped). BR, _ Thierry -- 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/b55522b5-f48f-3364-5a76-1d8358c6e5ee%40gmx.net.
