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.
On 01/06/2023 07:24, Jim Kingdon wrote:
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.
On 5/31/23 16:58, Mario Carneiro wrote:
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/.
On Wed, May 31, 2023 at 7:46โฏPM Humanities Clinic
<[email protected]> wrote:
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..
--
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/ef11fbc4-7c45-42bd-a982-06b714fa9aecn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/ef11fbc4-7c45-42bd-a982-06b714fa9aecn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/CAFXXJSsyni4-B%3DUjRE3V9sOoN9Xa6WWsRROaT3TC5ZZU4RzMZQ%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSsyni4-B%3DUjRE3V9sOoN9Xa6WWsRROaT3TC5ZZU4RzMZQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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/cbc3b950-d4e0-300a-760d-c1903d821328%40panix.com
<https://groups.google.com/d/msgid/metamath/cbc3b950-d4e0-300a-760d-c1903d821328%40panix.com?utm_medium=email&utm_source=footer>.
--
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/9172927b-997c-c0bd-08e0-4df01e6e419d%40gmx.net.
