In a typical textbook a group is defined as a set \(G\) with an associative operation such that two conditions hold:

A: there is an element \(e\in G\) such that for all \(g\in G\) we have \(e\cdot g = g\) and \(g\cdot e =g\). We call this element a "unit" or a "neutral element" of the group. B: for every \(a\in G\) there exists a \(b\in G\) such that \(a\cdot b = e\), where \(e\) is the element of \(G\) whose existence is guaranteed by A.

The validity of this definition is rather dubious to me, as condition A does not define any specific element \(e\) that can be referred to in condition B - it merely states that a set of such units \(e\) is not empty. Of course it does work in the end as we can prove that the set of such neutral elements has exactly one element, but still the definition by itself is not valid. You just can't reference a variable bound by a quantifier outside of the scope of that quantifier. One way around this is to first use condition A to define the notion of a monoid, then prove the uniqueness of \(e\) and then use the condition B to define groups.

Another way is to write conditions A and B together as follows: \(\exists_{e \in G} \ (\forall_{g \in G} \ e\cdot g = g \wedge g\cdot e = g) \wedge (\forall_{a\in G}\exists_{b\in G}\ a\cdot b = e).\)

This is rather ugly.

What I want to talk about is an amusing way to define groups directly
without any reference to the neutral elements. Namely, we can define
a group as a non-empty set \(G\) with an associative operation "\(\cdot \)"
such that
C: for every \(a,b\in G\) the equations \(a\cdot x = b\) and
\(y\cdot a = b\) can be solved in \(G\).
This theory file aims at proving the equivalence of this
alternative definition with the usual definition of the group, as
formulated in *Group_ZF.thy*. The informal proofs come from an Aug. 14, 2005
post by buli on the matematyka.org forum.

First we will define notation for writing about groups.

We will use the multiplicative notation for the group operation. To do this, we define a context (locale) that tells Isabelle to interpret \(a\cdot b\) as the value of function \(P\) on the pair \(\langle a,b \rangle\).

** Locale **group2

** defines **\( a \cdot b \equiv P\langle a,b\rangle \)

The next theorem states that a set \(G\) with an associative operation
that satisfies condition C is a group, as defined in IsarMathLib
*Group_ZF* theory.

** theorem ** **(in** group2**)** altgroup_is_group:

** assumes **A1: \( G\neq 0 \)** and **A2: \( P \text{ is associative on } G \)** and **A3: \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b \)** and **A4: \( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b \)

The converse of *altgroup_is_group*:
in every (classically defined) group condition C holds.
In informal mathematics we can say "Obviously
condition C holds in any group." In formalized mathematics the word "obviously"
is not in the language. The next theorem is proven in the context called
*group0* defined in the theory *Group_ZF.thy*. Similarly to the
*group2* that context defines \(a\cdot b\) as \(P\langle a,b\rangle\)
It also defines notation related to the group inverse and
adds an assumption that the pair \((G,P)\) is a group
to all its theorems. This is why in the next theorem we don't
explicitely assume that \((G,P)\) is a group - this assumption
is implicit in the context.

** theorem ** **(in** group0**)** group_is_altgroup:

{
** fix **\( a \) \( b \) ** assume **\( a\in G \), \( b\in G \)
** let **\( x = a^{-1}\cdot b \) ** let **\( y = b\cdot a^{-1} \) ** from **\( a\in G \), \( b\in G \) ** have ** \( x \in G \), \( y \in G \)** and **\( a\cdot x = b \), \( y\cdot a = b \)** using ** inverse_in_group, group_op_closed, inv_cancel_two
** hence ** \( \exists x\in G.\ a\cdot x = b \)** and **\( \exists y\in G.\ y\cdot a = b \)
** } **
** thus ** \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b \)** and **\( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b \)
** qed **

Definition of IsAssociative:
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \)
\( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \)
\( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)

Definition of IsAmonoid:
\( \text{IsAmonoid}(G,f) \equiv \)
\( f \text{ is associative on } G \wedge \)
\( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)

** assumes **\( e = \text{ TheNeutralElement}(G,f) \)

Definition of IsAgroup:
\( \text{IsAgroup}(G,f) \equiv \)
\( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)

** assumes **\( a\in G \), \( b\in G \)