How to Understand The "More Complicated" Expressions in Definitions

[Humanities Clinic]

Please pardon me for this rather basic question.

I have read https://us.metamath.org/mpeuni/mmset.html, especially on the sections "The Axioms", "The Theory of Classes". I have basic knowledge on set theory and classical logic, so I understand all the black symbols in prepositional and predicate, but I still find it difficult to understand some expressions in definitions.

For example, in https://us.metamath.org/mpeuni/df-grp.html:

Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+_g‘𝑔)𝑎) = (0_g‘𝑔)}

I know that Mnd, Base, +g, 0g etc. are all classes. But I don't get what it means for ∀𝑎 ∈ (Base‘𝑔) to be next to  ∃𝑚 ∈ (Base‘𝑔)(𝑚(+_g‘𝑔)𝑎) = (0_g‘𝑔)

What background knowledge am I still missing out which I should be reading, or did I miss out some material already on https://us.metamath.org/mpeuni/mmset.html? Please help me by pointing me to relevant reading material..

[Mario Carneiro]

The ∀𝑎 ∈ (Base‘𝑔) expression, or in ascii syntax "A. a e. (Base`g)" is the beginning of the restricted forall quantifier "A. x e. A ph" where you have highlighted just the "A. x e. A" part. It is read "for all x in A, ..." and denotes that some property "ph" holds for every x such that x e. A holds. In this case, the property in question is the remainder of the expression ∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔). In words, the expression says this:

The class "Grp" is defined to be the set of all g in "Mnd" (i.e. g being a monoid) such that for all a in the base set (carrier) of g, there exists some m in the base set of g such that m + a = 0, where + and 0 are the monoid operations on g.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ef11fbc4-7c45-42bd-a982-06b714fa9aecn%40googlegroups.com.

[Jim Kingdon]

The specific question of what it means for two restricted quantifiers to be next to each other is perhaps best answered by pointing to a simpler example like https://us.metamath.org/mpeuni/r19.12.html - the ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 there has the same syntax as ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)

If the problem, instead, is having trouble following df-grp in general, I think I'd advise not trying to go all the way from classes to df-grp in one step. A definition like df-grp builds on a variety of previous definitions (most notably https://us.metamath.org/ileuni/df-struct.html and https://us.metamath.org/ileuni/df-base.html and related definitions) and although it is true that Mnd, Base, +g, 0g etc. are classes, that only does so much to explain what they are doing in a particular statement.

One possible place to start is the section "A Theorem Sampler" at https://us.metamath.org/mpeuni/mmset.html#theorems . I can't offer any guarantees that starting with the theorems listed there, in roughly the order there, will be easier than jumping all the way to df-grp , but it may be worth a try.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsyni4-B%3DUjRE3V9sOoN9Xa6WWsRROaT3TC5ZZU4RzMZQ%40mail.gmail.com.

[Thierry Arnoux]

Mario and Jim already provided very good explanations. Let me send mine anyway!

A group is made up of two things: a set, which we call its "Base", together with an operation, which is the "+g".
We're using functions, so for a group g, Base(g) is the base set, and +g(g) is the operation.
In set.mm notation, these are written `(Base ` g)` and (+g ` g) respectively.

Now, a group is usually defined by 3 properties, on top of the "closure" property of the operation : Associativity, Identity Element, and Inverse Element.
A Monoid is defined by all these properties, except the "Inverse Element" property.
So our definition here states that a group is a monoid, having also the "inverse element" property.
This is expressed by the class abstraction `{ x e. A | ph }`. The variable `x` becomes our group `g`, `A` is the class of all monoids, `Mnd`, and `ph` expresses the "inverse element" property.

The inverse element property states that all elements of the base set admit an inverse. So, for all element of the base set `a`, there exists another element of the base set `m`, such that (in additive notation) `a+m=0`, where 0 is the identity element. In Metamath, that's written `(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)`.
The "there exists an `m` in the base set is written in the form of  a "restricted existential quantifier" `∃𝑥 ∈ 𝐴 𝜑`: `∃𝑚 ∈ ( Base ` 𝑔 ) (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔) `.
The "for all `a` in the base set is written in the form of an "restricted universal quanfitier" `∀𝑥 ∈ 𝐴 𝜑` : `∀𝑎 ∈ ( Base ` 𝑔 ) 𝜓`. Here the `𝜓` is itself a formula, namely `∃m ∈ ( Base ` g ) (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)`.
If one substitutes `𝜓` with `∃𝑚 ∈ ( Base ` 𝑔 ) (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)` in `∀𝑎 ∈ ( Base ` 𝑔 ) 𝜓`, one gets the `∀𝑎 ∈ ( Base ` 𝑔 ) ∃𝑚 ∈ ( Base ` 𝑔 ) (𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)`, where quantifiers follow each other immediately.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cbc3b950-d4e0-300a-760d-c1903d821328%40panix.com.