On Saturday, February 1, 2020 at 8:53:26 PM UTC-5, David Starner wrote: ...
I'm just > saying, if you want to learn group theory from Metamath, there's a lot > of stuff you're going to be fighting, and standard monoids, semigroups > and magmas are hardly going to be your breaking point.) > Thanks for your comments. I question whether semigroup is a standard thing that algebra students learn, since it is often omitted from textbooks, either because it is considered too trivial or too specialized, not sure. But in any case importing it isn't that big a deal in and of itself and would not have much impact on the big picture. I might agree to it anyway just to get the Bourbaki people off my back. :) (I think magma would be going to far, though.) My main concern is that it sets a precedent of introducing definitions that have no mathematical need driving them. There is no significant theory that follows from the trivial definition of semigroups; you show the associative law and you're done. The main reason given for so far for its introduction is that it simplifies the monoid definition one layer up, because otherwise the monoid definition is too confusing to understand, being a jumble of parentheses and conjunctions. First, df-mnd isn't even in the top 100 of complex definitions. If we set a precedent of introducing subdefinitions to simplify parts of bigger ones, where do we stop? Would we add hundreds of definitions defining trivial little pieces of larger definitions just because the larger definitions make some people dizzy? If we do, the reader would then have to learn both the name of each new definition as well as the property it specifies, instead of just the property as presented in the parent definition. I think it is usually more friendly to describe the properties informally in the description instead of introducing a somewhat cryptic acronym for each property. Second, df-mnd and other structure definitions aren't really meant to be studied directly in their raw form, which is a technical requirement in order to have nice self-contained objects that make things easier later on. Instead, the description of the definition should and usually does point to theorems that show the main properties that should be studied, such as the associative law in ~ mndass, which I think is quite easy to read. If we need to improve the descriptions to indicate that more clearly, I'm in favor of that. Norm -- 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/2cd5da7b-ff8f-4b4c-8dd3-45616eeeff46%40googlegroups.com.
