I want to comment on the following post in more detail:
On Saturday, February 1, 2020 at 12:39:46 AM UTC+1, Norman Megill wrote:
>
> 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.
>
I agree that the proper subset relationship would not be enough, but
together with the other results, there are a sufficiently high number of
theorems which would justify the definitions, in my opinion. Especially the
theorem about extended reals (~xrsmgmdifsgrp): its proof is scetched within
the comment of ~xrs1mnd, which actually calls for a formalization.
> 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.
>
I already started to prove that the even numbers/integers are a non-unital
ring (trivial, in principle, because 1 is not even ;) ). I do not plan to
provide a definition for them, although this would be appealing: I proved
already some "lemmas" which could become theorems if there was a definition
of even numbers.
>
> 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.
>
I do not know about Bourbaki's Theory of Sets, therefore I cannot rate it.
But only because you made bad experiences with Boubaki's set theory, this
does not mean that everything written by Bourkaki is bad.
> 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 found a book, called "Undergraduate Algebra", and it is published in
2019! The author is Matej Bresar from Slovenia (ISBN 978-3-030-14052-6).
Its table of contents starts with:
Part I The Language of Algebra
1 Glossary of Basic Algebraic Structures
1.1 Binary Operations
1.2 Semigroups and Monoids
1.2.1 Semigroups
1.2.2 Monoids
1.3 Groups
1.4 Rings and Fields
1.4.1 Rings
…
and this is exactly in line with our proposal: In section 1.1., the first
definition is the definition of a binary operation as mapping from S X S to
S. In the following text, he differentiate it from "external binary
operation", introducing the definition of closure. Although the word
"magma" is not used, I think the first two pages are about magmas in the
sense we use it. Afterwards (2nd definition), the associative law is
defined, followed by the commutative law (3rd definition). Finally, an
identity/neutral element is defined (4th def.). Section 1.2 starts with the
definition of a semigroup. In summary, Bresar first defines the "laws"
(properties of binary operations) and then, based on them, the
corresponding algebraic structures.
This is an excellent example for a very modern book, aimed at readers with
only basic mathematical knowledge...
Alexander
--
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/3704a858-31ba-4de9-b5ee-7d0a06d9e71e%40googlegroups.com.
