# Definition of a group written in formal logic

Is the formal logic in these axioms correct?

A group is a nonempty set $G$ with a binary operation $*$ that satisfies the following axioms:

• $(a * b) \in G \; \forall \;a,b \in G$

• $a * (b * c) = (a * b) * c \; \forall \; a,b,c \in G$

• $\exists \; e \in G : a * e = e * a = a \; \forall \; a \in G$

• $\forall \; a \in G \; \exists \; a^{-1} \in G: a * a^{-1} = a^{-1} * a = e$

In particular, in the last two axioms notice the difference of where the "for all" is placed.
The third axiom is meant to state that there exists an $e$ in $G$ that is a identity for all $a$ in $G$ under $*$.
While the last axiom is meant to state that for every $a$ in $G$ there exists an inverse $a^{-1}$ in $G$ under $*$.

• correct it is.... – tattwamasi amrutam Jun 11 '14 at 5:08
• If you are concerned about the formal logic I think you should be very careful with the placement of quantifiers. I would recommend rewriting the third statement as$$\exists \; e \in G : \; \forall \; a \in G : a * e = e * a = a$$and similarly for the first two. – David Jun 11 '14 at 5:13
• The axioms as given are not sentences of first-order predicate calculus. In particular, the placement of the universal quantifiers is not right. There is also nothing connecting the $e$ of the fourth axiom with the $e$ of the fifth. As a very informal description, it is sort of OK. From the formal point of view, quite far from right. – André Nicolas Jun 11 '14 at 5:15
• One can avoid the constant symbol by combining the last two sentences suitably into a single sentence. And a single binary function symbol is enough, if that's what we want. A more serious issue for formalization is the $\in$ symbol. In first-order group theory, one would omit all the $\in G$ stuff. – André Nicolas Jun 11 '14 at 5:34
• By definition, a binary operation on a set $S$ is a function $S \times S \to S$, so the first axiom is unnecessary. – Qiaochu Yuan Jun 11 '14 at 6:01