Regarding the possible introduction in the main part of semigroups and magmas: When I look at the page http://us2.metamath.org/mpeuni/df-mnd.html I feel a bit dizzy. The abundance of parentheses and conjunctions makes it hard to parse. Did you notice that the clause stating closedness is actually quantified over an extra z ? (This is of course innocuous, but still strange.) I find it much easier to look successively at http://us2.metamath.org/mpeuni/df-mgmALT.html and http://us2.metamath.org/mpeuni/df-sgrp.html and [the definition of Monoid from Semigroup -- Alexander: can you add it?]. So, to me, there is already a pedagogical benefit, even if no theorems are proved. I find these piecemeal definitions easier to learn. Once you grab the final concept, you can forget about the intermediate steps. I.e., you do not have to remember what a magma or semigroup is, if you don't want. This was only an aid in the process of getting the definition of a group.
Regarding Norm's remark on Bourbaki: Indeed, their set theory is known to be awkward. None of its members were logicians or set theorists, and they just wanted to "get this done" before moving to what they considered more interesting math. By the way: you actually use a lot of Bourbaki's terminology and notation in set.mm: the symbol for the empty set, the blackboard bold typeface, the terms "ball" and "sphere" in metric spaces, the terms injection/surjection/bijection, etc. Actually, new terms were carefully chosen, and as much as possible simple words from everyday life, like "magma" (because volcanic magma looks structureless), "ball", even when they are not round (the previous term was some impossible jargon), in/sur/bijection (previous terms were similar jargon). The terms "barrel" (a barrel is closed, convex, balanced, absorbing: this makes as much sense in everyday life as in formal math), bornivorous, etc. I think that Bourbaki was somehow victim of its success: it was so influential that after a few years or even decades, people took it for granted that there was a common language and notation for all the branches of mathematics. But I think it is easy now to underestimate the novelty that it was in the 1930s and 1940s. Of course there was already work on logic. And of course each specialist in his domain was ahead of what was meant to be a treatise of "dead mathematics". Discoveries also spread slower at the time: the internet was a bit slower in those days, notwithstanding political considerations... 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/0f67dbc1-5ec5-4dc4-a35f-0117fabe444d%40googlegroups.com.
