Ring vs. Rng (deferred)

[avekens]

According to the Google group discussion https://groups.google.com/d/msg/metamath/XKl7K0qx4uc/hRykryMhDgAJ (see also issue #866), the currently used abbreviation "rng" for a unital ring Ring should be replaced by "ring".

As a first step, I provided the definition of a general, i.e. not necessarily unital , ring Rng (see ~df-rng0 in my mathbox). For this, I needed the definition of a "Semigroup" (the mutiplicative group of a general ring is a semigroup), so I added this, too (SGrp, see ~df-sgrp). Doing this, I also added a definition of a "Magma" (Mgm, see ~df-mgmALT). Here are conflicts with the deprecated definition of a magma which have to be cleaned up. For all changes see PR # 1388.

If there is no objection, I would move these definitions and the related theorems into the main part of set.mm in the next step, changing the labels: df-rng -> df-ring, df-rng0 -> df-rng (and df-mgm -> df-magma, df-mgmALT -> df-mgm, etc.). I would also update the table of abbreviations in section "17.1.1 Conventions" accordingly. Maybe some of the current "rng" theorems are already valid for Rngs, so that they can be moved up into the corresponding subsection (and need not to be renamed).

Afterwards, the renaming of the labels containing "rng" could start.

@benjub @nmegill @digama0 @david-a-wheeler @tirix OK?

[benjub]

Sounds good to me. Thanks @avekens

[avekens]

After I bought Bourbaki ;-) I decided to go 2 steps back beyond the definition of magmas and start the definitions and theorems for algebraic structures with "laws" and "internal binary operations", according to Bourbaki, but also to Marshall Hall Jr. in "The Theory of Groups". This seems to be also the approach in the deprecated section "18.1.5 Group-like structures", which I will clean up on moving my definitions to the main body of set.mm.

I defined 3 laws:

• clLaw
• assLaw (corresponds to deprecated Ass)
• comLaw

and 3 kinds of internal binary operations:

• intOp
• clIntOp (corresponds to deprecated Magma)
• assIntOp (corresponds to deprecated SemiGrp)

The laws can be used to specify the operation slots of extensible structures, resulting in slightly modified definitions for magmas and semigroups:

• df-mgm2 $a |- MgmALT2 = { m | ( +g m ) clLaw ( Base m ) } $.
• df-sgrp2 $a |- SGrpALT2 = { g e. MgmALT2 | ( +g g ) assLaw ( Base g ) } $.

Everything can be found in my Mathbox, see PR #1428. I would like to move these definitions to the main body of set.mm after the changes are merged.

The three operations can be used if an operations of an extensible structures is a function, e.g. ( +f M ) e. ( assIntOp ( Base ` M ) ) would hold.

If there are no objections, I will start to move the corresponding parts of my mathbox to the main body of set.mm and to clean up section "18.1.5 Group-like structures" accordingly (taking care that I will retain the original contributors, where appropriate). When I have finished this task, I think we made a big step towards a more Bourbaki-like structure of set.mm, at least regarding the Algebra part.

By the way, Is the term "internal operation" really common in the English literature? I often find the term "binary operation" only (see, for example, [Bruck] p. 1: "By a [[...] binary operation [[...] on the [[...] set G we mean a siungle-valued mapping [[...] from [[...] G X G into G."). The term "binary operation", however, could also be understood as function of two arguments from not necessarily different sets (if the sets are different, the operation is explicitly called "external binary operation" (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations ).
So it seems natural to call a binary operation with two arguments from the same set "internal (binary) operation". In set.mm, the term "internal operation" is used very often. In German, it is called "innere (zweistellige) Verknuepfung", in French "Loi de composition interne". Does anybody knows an article or a book in which the term "internal (binary) operation" is used?

[digama0]

I'm not really seeing why this should be in main set.mm. I deliberately avoided defining semigroups when setting up the algebraic hierarchy because we have no present use for them. This applies also for non-unital rings, magmas, and these even more abstract associativity law constructors.

While you are free to play with these concepts in your mathbox, I would really like to see some application before moving them to main. Just because there is a wikipedia page on them or Bourbaki defines them doesn't mean they are useful for set.mm. (In my opinion, Bourbaki goes overboard with the abstraction in many places. Abstraction without application leads to poor APIs.)

[benjub]

I'm not sure that it is useful to define clLaw, assLaw, comLaw, intOp, clIntOp, assIntOp. But I think it is worth definining the class of magmas and the class of semigroups. Even as mere building blocks towards monoids and groups, I think it makes things clearer.

As for nonunital structures, I think they have enough applications. Right now, I can think of the Gelfand representation of C*-algebras, for instance. There is a large amount of research in semigroup, even if this is maybe not central to mathematics. As for non-associative structures, there are results in non-associative algebras. I do not remember if Bourbaki uses often his results about magmas, for instance in the theory of Lie rings and algebras.

On whether moving them to the main part when there is no application in set.mm yet, I do not know. Note that putting them now in the main part will hopefully avoid that someone in the future, while working on some applications, misses this ground work and redoes it himself.

[digama0]

As for nonunital structures, I think they have enough applications. Right now, I can think of the Gelfand representation of C*-algebras, for instance. There is a large amount of research in semigroup, even if this is maybe not central to mathematics. As for non-associative structures, there are results in non-associative algebras. I do not remember if Bourbaki uses often his results about magmas, for instance in the theory of Lie rings and algebras.

I have no doubt that there is meaningful mathematics that can be done with these structures. (I question this in the case of magmas though. They are literally just binary functions.) My point is that none of this is in set.mm, and I don't know but I don't get the impression you are working on these topics.

The point here is to have a development be spurred by an immediate need to formalize some other area (in the yak shaving sense). This process guides the way you state theorems so that they are useful to users, not just abstractly nice-looking. It is difficult to anticipate what will be needed until you actually need it, and guessing usually just leads to a lot of wasted effort up front that may not even pay off later.

If you think it makes things clearer, by all means develop these topics in your mathbox. Just because Mnd doesn't currently use any definition of semigroup, doesn't mean you can't prove an alternate definitional theorem for them that does, without touching df-mnd itself. If and when you get some nontrivial mathematics done on these low level structures that is generally useful and gets use in another area or by another person, that would be a good time to move to main, because at that point it will already be a relatively mature development.

[avekens]

I do not want to restart the intense and partially offending discussion conducted in the Google group several years ago, but I think this is mainly a philosophical discussion: what is the meaning of "use/usefulness of (basic) concepts" or "meaningful application of (basic) concepts"? This discussion reminds me of discussions if "basic research" or "aerospace engineering" is necessary or useful, and why billions of dollars should be spent for it (and not for "real" problems as fighting against hunger, injustice and wars in the world).

But comming back to an objective discussion. Here are some arguments in favour of providing the concerned definitions/theorems in main set.mm:

"laws":

• This is what I have learned in Algebra at school, long before I heard about Groups, Rings, etc.
• Formalization of the terms "closure", "associative", "commutative", etc. which are used throughout set.mm
• making definitions of (and many proofs for) corresponding extensible structure clearer and shorter

"internal binary operations":

• generalization of "+f"
• making definitions/theorems in Part 18 obsolete, so that they can be removed

"magmas, semigroups"

• many books start with these concepts, not only Wikipedia and Bourbaki (e.g. [Hall], [Bruck], ...)
• propositional logic, predicate logic and set theory also starts systematically from the beginning, and not in between as done for algebraic structutres (starting with monoids)
• making definitions of (and many proofs for) advanced extensible structures based on these concepts clearer and shorter: To use these concepts for enhancing them to get the already existing concepts is a meaningful application!
• semigroups are needed to define non-unital rings
• the term "magma" is often used in main set.mm, and there are also some theorems about magmas (with lables containing the acronym "mgm"): so why not define it formally?

I made a concrete experience in the direction Benoit pointed at ("that someone in the future, while working on some applications, misses this ground work and redoes it himself") when I proved "The binomial theorem for semirings": I needed the binomial theorem only for (unital) rings, and it would have been much easier to prove it using the already available theorems for (unital) rings. But since this theorem holds already for semirings, I wanted to prove it only using the properties of semirings - but I had to build up the whole infrastructure for semirings by myself. I would have been glad if this had been already available.

To conclude, I want to make the following proposal:

1. we should at least agree on moving the definitions of magmas, semigroups and non-unital rings (and the related theorems) to the main body of set.mm, as proposed by Benoit. In a second step, theorems available for monoids and unital rings which are already valid for magmas, semigroups and
   non-unital rings can be revised (i.e. generalized as new theorems, used to shorten the proofs
   of the existing theorems). By this, there is no impact on any existing theorems.
2. I would also like to have the "laws" in main set.mm, because they are so basic/elementary. To have them would also justify to delete the corresponding definitions/theorems in the deprecated part 18.
3. I could do without the intOp-Definitions and theorems for the moment, leaving them in my mathbox.

Is it acceptable if bullet points 1. and 2. are realized? How can we proceed if we find no agreement?

[nmegill]

I have been asked to step into this discussion, so I will weigh in with my opinion.

As a general comment, I have typically been very conservative, even overly so, about introducing new definitions, and have often postponed introducing them until the advantage became overwhelming (in particular could reduce the size of set.mm), at which point I would retrofit theorems that could benefit.

Every new definition is an extra burden on the reader/user, a new formal thing that must be learned as well as extra overhead in set.mm. So it should have a clear benefit.

This is expressed in ~ conventions: "New definitions infrequent. Typically, we are minimalist when introducing new definitions; they are introduced only when a clear advantage becomes apparent for reducing the number of symbols, shortening proofs, etc. We generally avoid the introduction of gratuitous definitions because each one requires associated theorems and additional elimination steps in proofs. For example, we use < and ≤ for inequality expressions, and use ((sin‘(i · 𝐴)) / i) instead of (sinh‘𝐴) for the hyperbolic sine. "

[Note that we will never introduce > and >= because they offer no proof shortening benefit but instead would explode the number of support theorems with mixed < and >. Instead, we use the comment to state in English "greater than" when it makes sense. We would readily introduce sinh if it was frequently used in some theory, especially if proofs would be shortened as a result, but that hasn't happened yet.]

"laws":

• This is what I have learned in Algebra at school, long before I heard about Groups, Rings, etc.
• Formalization of the terms "closure", "associative", "commutative", etc. which are used throughout set.mm

The statement of the law "(A+B)+C=A+(B+C)" seems less obscure than saying "<. .+ , S >. e. assLaw". The latter means the reader now must look up yet another definition and memorize it. The comment almost always says "Show the associative law holds" or the like, and to me that is clearer and preferable to introducing yet another formal definition. BTW in introductory algebra books I haven't seen things like assLaw formally defined; it's always been in English, just as we do in the comments.

Even if it is formally defined in some books, that doesn't mean that we need to add it to set.mm. Personally I prefer to see definitions introduced as applications arise for them. The intent has never been to make set.mm a formalized glossary of all the terms in Bourbaki or Wikipedia, which would be a major shift in philosophy.

• making definitions of (and many proofs for) corresponding extensible structure clearer and shorter

"(A+B)+C=A+(B+C)" seems pretty clear to me, along with the word "associative" in the description. And we need to show "(A+B)+C=A+(B+C)" anyway, so it is extra work to additionally show "e. assLaw".

If you can demonstrate that the development of say group theory could use assLaw to reduce the file size of set.mm, I would be more receptive. I am not convinced that it will.

"internal binary operations":

• generalization of "+f"
• making definitions/theorems in Part 18 obsolete, so that they can be removed

The reason Part 18 is obsolete is because they have been superseded by extensible structure versions. The intent is for theorems in Part 18 to be removed when someone goes through them and verifies that we have an extensible structure version, or adds the extensible structure version if it is missing, or determines the Part 18 theorem isn't useful and should just be deleted.

There was never any intention of replacing Part 18 with yet another layer of similar definitions, because it would be redundant given the existing extensible structures. That's why I was a little puzzled about why you were referencing Part 18.

"magmas, semigroups"

• many books start with these concepts, not only Wikipedia and Bourbaki (e.g. [Hall], [Bruck], ...)

And many books don't. The books for introductory algebra courses (sometimes intended for an audience that includes engineers and physicists) that I've seen usually define a group in the beginning and start with that. More advanced books may define magma, etc. in English to have some terminology to talk about things (like we have the terminology "binary operation" etc. in the comments) but I think it is rare that they formally define set-theoretical classes for all such terminology and use those formal definitions in the statement of theorems.

In particular, we already have a large, useful development of binary operations. It seems that Magma is redundantly introducing formalism where none is needed, but at the expense of a larger set.mm size to restate theorems we already have and placing an extra burden on the reader to memorize yet another definition and learn associated theorems. We already have the notation ".+ : ( f X. f ) --> f", which isn't that much longer to state than ".+ e. Magma". And we don't need to state that very often once we prove basic closure theorems for an extensible structure. More importantly, our function notation needs to be learned anyway and thus is obvious by inspection when encountered in a structure definition, whereas Magma is not so familiar to everyone.

• propositional logic, predicate logic and set theory also starts systematically from the beginning, and not in between as done for algebraic structutres (starting with monoids)

That is because they are the starting axioms for everything we do, and I chose to express them in primitive language ideally before getting into the complexities of class notation. It lets the reader see directly what an axiom actually "is" formally, without having to unwind layers of definitions. It was my personal choice to present it that way. Some ZFC developments start with axioms stated with defined terms, which I found confusing when I was naive about such things (especially when they are vague like "an infinite set exists"). In the comments for most set theory axioms we also point the user to versions using defined terms.

But actually we did originally start from "the beginning" in the case of Grp, which used to be defined directly using only set theory language and no algebraic language. Later on we introduced Mnd, then redefined Grp in terms of it. It was relatively trivial to do that. If additional layers (e.g. semigroups) become useful in the future, we can redefine it again.

I actually still have a few mixed feelings about defining Grp in terms of Mnd, because a physicist who just wants to know what a group is wouldn't want to have to peel apart layer after layer of abstract definitions to finally understand it. To that end, I was careful to make sure we at least had theorems defining groups directly and not in terms of more general structures that would need to be unwound.

• making definitions of (and many proofs for) advanced extensible structures based on these concepts clearer and shorter: To use these concepts for enhancing them to get the already existing concepts is a meaningful application!

Again, that is the role of the theorem description. Formalizing terminology regardless of benefit seems like busywork that makes the reader's life more difficult for no good reason.

• semigroups are needed to define non-unital rings

I'm not up-to-date enough to know whether this is advantageous, and am not very familiar with the applications of non-unital rings. We can always define Rng as directly as we need to, like we use to do with Grp, then if a separate application using semigroups is developed, we can exploit its theorems by redefining Rng. Again, not a big deal to do that, and in the meantime the reader has fewer intermediate definitions to learn.

Do we even have a use for Rng right now? If its only current purpose is to shorten the definition of Ring then I would say that it's premature to import it into the main set.mm. Again, it's not a big deal to alter extensible structure definitions to exploit more general structures - that's part of the extensible structure design.

• the term "magma" is often used in main set.mm, and there are also some theorems about magmas (with lables containing the acronym "mgm"): so why not define it formally?

Because the comment is sufficient to describe it, and we have a theory of binary operations already well developed.

It isn't a problem for me if people want to formalize normally informal terminology in their mathboxes, which are intended to provide freedom to experiment. But I don't buy the argument that if it's hidden in a mathbox, no one will see it and duplicate effort will result. I don't know of any time that has ever happened. Almost always users will search (or should search) the comments for terminology in the areas they are interested in, and anything in mathboxes with the terminology will show up. No one will know that "assLaw" is what should be searched for, whether it is in the main set.mm or resides in a mathbox; instead people will search comments for "associative".

[david-a-wheeler]

On Wed, 22 Jan 2020 09:14:26 -0800, nmegill notifications@github.com wrote:

As a general comment, I have typically been very conservative, even overly so, about introducing new definitions, and have often postponed introducing them until the advantage became overwhelming (in particular could reduce the size of set.mm), at which point I would retrofit theorems that could benefit.
Every new definition is an extra burden on the reader/user, a new formal thing that must be learned as well as extra overhead in set.mm. So it should have a clear benefit.
[Note that we will never introduce > and >= because they offer no proof shortening benefit but instead would explode the number of support theorems with mixed < and >. ...
Even if it is formally defined in some books, that doesn't mean that we need to add it to set.mm. Personally I prefer to see definitions introduced as applications arise for them. The intent has never been to make set.mm a formalized glossary of all the terms in Bourbaki or Wikipedia, which would be a major shift in philosophy.
In particular, we already have a large, useful development of binary operations. It seems that Magma is redundantly introducing formalism where none is needed, but at the expense of a larger set.mm size to restate theorems we already have and placing an extra burden on the reader to memorize yet another definition and learn associated theorems.
Formalizing terminology regardless of benefit seems like busywork that makes the reader's life more difficult for no good reason.

I think there may be a middle ground here, at least in terms of of constructs like >, >=, sinh, and maybe magmas.

I would like set.mm to include a formalized glossary of at least all "widely used mathematical constructs that could have sensible set.mm definitions". I would like to see set.mm to serve as a kind of standard and transmission to the future of formalized math knowledge. But I also agree that restating many theorems to use them would produce a very long & possibly hard-to-follow result. I even helped write the conventions text about preferring to avoid new definitions and why that's so :-).

We could add at the end of set.mm a section about "Other common definitions",
where each entry would have "(New usage is discouraged.)".
Within that section would be a collection of selected widely-used math terms and
their definitions for purposes of set.mm (and maybe 1-3 theorems to demonstrate them).
That way, if someone says "what is greater than?", we have a formally-defined answer.

Why bother?

1. The set.mm database uses a lot of these terms in the comments (>, sinh, etc.),
   but they aren't formally defined anywhere. It'd be clearer if we did define them.
2. This means that someone trying to translate some other math statement
   into set.mm has a formal statement to start with.
3. It clearly defines these terms for future generations.
4. This does not significantly increase the size of set.mm and it does not require set.mm users to remember these "other common definitions". It would be a small explanatory appendix.

[benjub]

I will not enter the details of the discussion, but I see arguments like "this is not the intent" or "the reader will"... Therefore, I think it should first be clarified what the goals of set.mm are and what its intended readership is. I asked for this in one of my first posts (https://groups.google.com/d/msg/metamath/LcbK2gJYvZA/V8Y_SlqRAQAJ), for roughly the same reasons, but never got an answer.

It is at the same time difficult and essential. Most things would follow from an enunciation of the main goals, maybe a roadmap (short/long term goals), and the intent. For instance, it is not possible to have something which is good both as a pedagogical tool and as a reference (e.g., Bourbaki is a great reference treaty, but a terrible pedagogical tool, and was never intended to be one). So choices will have to be made, and sometimes, compromise is worse than either option.

The mere effort to draft such a list of goals, intents, and intended readership could in itself be beneficial, since it forces us to think about it from a wider angle. Another example: you cannot speak in an appealing way to both a mathematician wanting to learn formalization and a computer scientist wanting to learn math.

As long as we do not have clear goals, discussions like this will reappear, and will keep being sterile.

[avekens]

Thanks a lot for everybody expressing your opinion on this topic. I have the feeling that we cannot achive an agreement on this specific issue (Magma, Semigroup, Ring, binary operation, etc.) yet - we have to clarify what the goals of set.mm are in general, as Benoit proposed.

Therefore I suggest to stop the discussion here (within this issue) and start/contuinue it at another place (Google group, or a separate issue). As a consequence, I will not move any of the mentioned definitions/theorems to the main body of set.mm yet. This issue should remain open (marked as "deferred") until a general decision is made.