On Fri, Jan 31, 2020 at 6:07 PM Norman Megill <[email protected]> wrote:
> What I fear happening is that we've introduced unnecessary additional
> complexity for anyone just wanting to learn about groups (such as an
> engineer). What was a straightforward definition turns into a tower of
> associated structures they've never heard of (monoid, semigroup, magma) and
> don't care about, but are forced to learn. Will they give up and go
> elsewhere (e.g. an undergraduate book on group theory that simply starts with
> groups at the beginning)? Even monoids are apparently a graduate-level topic
> based on Lang's books.
I'm here in part because I failed to make the step from undergraduate
mathematics to graduate-level mathematics; I was forced to take my
B.S. in math and go. Group theory/modern algebra is something I'd like
to learn, and sort of have been faffing about for many years now. From
my perspective, Metamath introduces a whole pile of stuff into group
theory; it's constantly worrying about predicate logic and set theory
at a level introductory modern algebra just ignores, combined with a
whole bunch of Metamath details and stuff; it's actively harder to
read than raw TeX, and I suspect your engineer doesn't like reading
raw TeX, either. I'm here because if I can prove some of this stuff, I
can feel like I'm doing something of value and it will hopefully help
me nail down exactly what it means in my head. There's good argument
that for me, Metamath is yak shaving, a way of avoiding actually
working on learning any one field of math intensely. I would actively
discourage anyone from using Metamath to learn group theory, maybe
unless they were of the same inclination, to use it as a way to have
full understanding of the subject formally checked. I don't think
that's engineers; I think that's mainly people like me who have read
books on set theory (including New Foundations) and the consequences
of the Axiom of Choice and GΓΆdel's theorems, those that are looking at
group theory from a hardcore math perspective, not an engineering
perspective, and I don't think adding monoids, semigroups, and magmas
are going to make much difference.
(And if you are worried, take CycGrp = {π β Grp β£ βπ₯ β (Baseβπ)ran
(π β β€ β¦ (π(.gβπ)π₯)) = (Baseβπ)}. Grp is obvious enough, but
CycGrp? ran?* I could derive what (π(.gβπ)π₯) means from context,
but it took a lot of clicking on definitions to fully get that
(π(.gβπ)π₯) is applying a binary function to n and x, and that
function .g is group exponentiation, not the group operation. 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.)
(Oh, and your engineer, depending on discipline, may be familiar with
monoids, since they're big in functional programming; see e.g.
https://fsharpforfunandprofit.com/posts/monoids-without-tears/ )
* Ken Thompson was once asked what he would do differently if he were
redesigning the UNIX system. His reply: "I'd spell creat with an e."
--
Kie ekzistas vivo, ekzistas espero.
--
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/CAMZ%3Dzj7RyJnwiBqL9GhPJCXGMGbNC7osz6jB4jqLTQQWhdGiaw%40mail.gmail.com.
