Your counterexamples to show non-membership are interesting. I appreciate
your work dong this, and certainly it would accompany the magma and
semigroup structures should we decide to import them. However, showing the
proper subset relationship in and of itself still doesn't quite yet show us
that we have a true need for these structures.
For example, if we defined EE as the set of even numbers, we could have a
theorem showing it is a proper subset of ZZ, but such a theorem isn't
enough in itself to justify introducing it. We would want a sufficient
number of theorems about even numbers whose statements would become
significantly shorter and clearer. That hasn't happened and probably
won't. Just because the terminology "even number" appears in the
literature doesn't mean we have to have a special symbol for it; instead,
"2 || N" suffices.
Regarding Bourbaki: A long time ago, before Metamath, I eagerly and
naively started off trying to learn the Theory of Sets before knowing any
formal logic or set theory. Its bizarre "assemblies" (tau notation) are
extremely inefficient and seem to ignore all the developments in FOL and
axiomatic set theory that were already essentially mature and standard in
the rest of the world. With much effort and the assistance of a computer
program I wrote, I worked out the thousands of symbols needed to define the
empty set. Then I gave up when I realized the number 1 would be unfeasible
(it turns out to require trillions of symbols). Even with intermediate
definitions to shorten things, I was unable to gain an intuitive
understanding of what was going on.
After I learned "real" set theory, I became somewhat less than enamored
with Bourbaki, so I mention this experience in the spirit of full
disclosure. :) With that said, the feeling I get is that Bourbaki
sometimes does its own thing that may or may not appear in mainstream
mathematical literature. My personal preference is not to use Bourbaki as
a primary reference for terminology and notation, unless it is also
standard in modern textbooks.
Two relatively modern and well-regarded textbooks are Lang's "Undergraduate
algebra" (~400 pp) and his graduate-level "Algebra" (900 pp). The first
book starts off defining "group", and the second starts with "monoid".
Neither book mentions "magma" or "semigroup". Even "monoid" is apparently
a topic too specialized for Lang's undergraduate book, which doesn't
mention it at all.
I would like to hear other opinions on whether "magma" and "semigroup"
should become part of the main set.mm body.
Norm
On Friday, January 31, 2020 at 2:01:03 AM UTC-5, Alexander van der Vekens
wrote:
>
> For the last week I have been "actively working" on providing
> "applications" of the definitions and related theorems for magmas and
> semigroups (I've spent almost my whole spare time for it). Although the
> results may be trivial, they are "serious", at least in my opinion.
>
> I've provided the results in my latest two PRs (they can be found in my
> mathbox). Here they are (in brief):
>
> - There is a small magma (with a base set containing two elements)
> which is not a semigroup: ~mgm2nsgrp
> - There is a small semigroup (with a base set containing two elements)
> which is not a monoid: ~sgrp2nmnd
> - The previous results prove the proper inclusion chain `Mnd C. SGrp
> C. Mgm`: ~mndsssgrp and ~sgrpssmgm
> - The (additive group of the) extended reals is a magma, but not a
> semigroup. Formalization of the statements in the comments of ~xrsmcmn and
> ~xrs1mnd: ~xrsmgmdifsgrp
> - A stronger version of ~ gsumpropd if at least one of the involved
> structures is a magma, see ~gsumpropd2: ~I mention this in the spirit of
> full disclosure. :)
>
> Especially the proof of ~sgrp2nmnd was time-consuming, although not
> difficult/complex: 32 "sums" had to be"calculated" to show the
> associativity (see ~sgrp2nmndlem4).
>
> Now I want to ask if these results are sufficient to move the definitions
> and basic theorems for magmas and semigroups (and the results themselves,
> of course) to the main body of set.mm? From my point of view, they
> should, at least in they plain variants (~df-mgmALT, ~df-sgrp), without
> using the "law" definitions (although I like them very much, there is still
> no "serious" use of them, and they can be introduced easily later when they
> are really required). And afterwards, many theorems proven for/in the
> context of monoids could be tidied up accordingly.
>
> For rings (non-unital vs. unital) I plan to provide similar results, maybe
> also a result in category theory ("the category of rngs has a zero object
> while the category of rings does not" as proposed by Benoit) - but
> unfortunately, even the category of rings is not available in set.mm
> yet...
>
>
>
--
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/e5b0c89e-7fb6-4b24-84bb-0bf0bb06217d%40googlegroups.com.
