Just a short comment before I have to go out (see below)... On Saturday, February 1, 2020 at 2:23:08 AM UTC+1, Benoit wrote: > > 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?]. > Yes, I'll add it! I had this in mind for some time, but I didn't consider it necessary. But now I think it may be the sticking point for this discussion. Having a first glance at it, I discovered that ~df-mnd is currently used in theorem ~ismnd only (in the main body of set.mm)! Therefore, it can be simply replaced by { g e. SGrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }, and the proof of ~ ismnd can be rewritten to use this definition instead of the current one. Therefore, all theorems using ~ismnd are not affected at all. And as for many definitions in set.mm, the definition needs not to be understood by beginners (see my ~df-mamu example above) - if they look at the defining theorem ~ismnd, they find everything they need in a clear way (much clearer than in the current ~df-mnd). Furthermore, the definition of groups ~df-grp is also not affected at all, because it is based already on the definition of monoids ( `Grp = { g e. Mnd | ... `).
As a conclusion, there will be more definitions and theorems about magmas and semigroups (for interested readers), but only one significant change (definition of monoids) for beginners/readers not interested in magmas and semigroups, which can be, however, ignored by them if they only look at ~ismnd (if at all - if they are interested in groups only, actually nothing will change). > 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. > -- 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/965075ee-b224-446c-b08c-438fbcb45e28%40googlegroups.com.
