This is my first experiment in presenting formalized mathematics in a blog post. Ideally, such presentation should be generated by the theorem proving environment from machine-verified sources. Since the software for converting Isabelle theory files to WordPress postable HTML is not ready yet, the post below is a result of conversion done manually.

```
```**theory** Group_ZF_1 **imports** Group_ZF

**begin**

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

**A:** there is an element such that for all we have and . We call this element a “unit” or a “neutral element” of the group.

**B:** for every there exists a such that , where is the element of 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 that can be referred to in condition B – it merely states that a set of such units is not empty. Of course it does work out in the end as we can prove that the set of units 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 and then use the condition B to define groups.

Another way is to write conditions A and B together as follows:

This is rather ugly.

The third way that 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 with an associative operation “” such that

**C:** for every the equations and can be solved in .

This blog post aims at proving the equivalence of this alternative definition with the usual definition of the group, as formulated in IsarMathLib’s Group_ZF.thy. The informal proofs come from an Aug. 14, 2005 post by buli on the matematyka.org forum.

**An alternative definition of a group**

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

```
```**locale** group2 =
**fixes** P
**fixes** dot (infixl 70)
**defines** dot_def [simp]:

The next theorem states that a set with an associative operation that satisfies condition C is a group, as defined in IsarMathLib’s Group_ZF theory.

```
```**theorem** (in group2) altgroup_is_group:
**assumes** A1: and A2:
**and** A3:
**and** A4:
**shows**
**proof** -
**from** A1 **obtain** a **where** D1:
**with** A3 **obtain** x **where** D2: and D3:
**from** D1 A4 **obtain** y **where** D4: and D5:
**have** T1:
**proof**
**fix** b **assume** A5:
**with** D1 A4 **obtain** y_{b} **where** D6:
**and** D7:
**from** A5 D1 A3 **obtain**** x**_{b} **where** D8:
**and** D9:
**from** D7 D3 D9 D5 **have**
**and**
**moreover** **from** D1 D2 D4 D8 D6 A2 **have**
**and**
**using** IsAssociative_def
**moreover** **from** D7 D9 **have**
**and **
**ultimately** **show**
**qed**
**moreover** **have**
**proof** -
**from** D2 T1 **have**
**also** **from** D4 T1 **have**
**finally show**
**qed**
**ultimately** **have**
**with** D2 A2 **have** **using** IsAmonoid_def
**with** A3 **show**
**using** monoid0_def monoid0.unit_is_neutral IsAgroup_def
**qed**

The converse of theorem altgroup_is_group: in every (classically defined) group the 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 IsarMathLib’s theory Group_ZF.thy. Similarly to group2 that context defines as , where is the group operation. It also defines notation related to the group inverse and adds the assumption that the pair is a group to all its theorems. This is why in the next theorem we don’t explicitely assume that is a group – this assumption is implicit in the group0 context.

```
```**theorem** (in group0) group_is_altgroup: **shows**
**and**
**proof** -
**{** **fix** a b **assume** A1:
**let** x =
**let** y =
**from** A1 **have**
**and**
**using** inverse_in_group group_op_closed inv_cancel_two
**hence** **and**
**}** **thus**
**and**
**qed**

```
```**end**

This blog post has been generated from IsarMathLib’s Group_ZF_1.thy theory file, see the relevant pages of IsarMathLib proof document.

See also the TiddlyWiki rendering of this post.

## Leave a Reply