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.
