To answer FL's latest message: the first and foremost thing that Norm has done and still does for us is having created the Metamath language, continuously improving the Metamath C program (the "official implementation" of the Metamath language), and having begun and still being the main contributor (in number of theorems contributed) of the database set.mm. And he's doing all of this voluntarily, benevolently, with open and free licensing.
Then, and only then, FL might have a point in that sometimes, it feels like Norm chooses the one reason that will make a definition rejected from the main part. By now, we know the usual reasons: not pedagogical for engineers/undergrads, not enough applications in set.mm, does not simplify other proofs enough, can be coded "not-too-difficulty" in terms of previous definitions, etc. Since there will most often be at least one criterion not fulfilled by a given definition, it is easy to pick one of these reasons to reject almost any definition. This is why I asked for the goals of set.mm, to have some clarity. As for Norm's question: "Question: why do you think that Lang's Algebra (2002 edition) doesn't define or mention "semigroup" in its 900 pages?": [I'm using your edition for the page numbers.] On page 3, he defines (terms in boldface): - law of composition - associative - unit element and finally he defines, verbatim, "A monoid is a set G, with a law of composition which is associative, and having a unit element". So, even if the words "magma" and "semigroup" are not there, this looks furiously like a piecemeal definition, using the three steps successively, and they effectively correspond to respectively "magma", "semigroup", "monoid". He doesn't introduce these terms because he does not study them (they are of course less important than groups, rings, etc.). Also, note that the symbols \forall and \exists appear almost never (or maybe even never) in the 900 pages. Therefore, his readers are not faced with intimidating long strings of formal symbols, and he doesn't need to introduce "magma" and "semigroup" as aids. By the way: I just noticed that he uses the symbol \subset in a reflexive sense (page ix). Therefore, I'm happy that I insisted a few months ago, against the opinions of several people here (https://groups.google.com/d/topic/metamath/_OqalbIKkgE/discussion), to remove this symbol from set.mm because of its ambiguity, and to replace it with \subsetneq (because that's what it meant in set.mm!) -- the symbol for the reflexive relation remaining \subseteq. Benoît -- 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/5e69ff34-2e33-4e28-b3e3-2b73ae4359b2%40googlegroups.com.
