A formal proof in Group Theory

Lasse Nielsen & Morten Ib Nielsen

Department of Computer Science, University of Copenhagen

June 20, 2006

1 Introduction

In this report we set out to formally prove a simple result of Group Theory namely:

Theorem 1.1 Let e be a neutral element of a Group G then e is unique. Thus we can talk about the neutral element of a Group G.

The theorem above is very loosely formulated. In this report we set out to formalize the theorem and give a formal proof of it’s correctness. In order to do this we need to do a lot of other work. First in XXTODO we define Propositional Calculus and then in MMTODO we define First order Predicate Calculus. Then using this we define ZFC set theory in YYTODO and finally having set theory available we can define a Group in ZZTODO. Then in WWTODO we restate the above theorem in a formal setting and we give a formal proof of it’s correctness.

TODO mere jalla.

2 Propositional Calculus

Based on mathworld^{1} and thus on Kleene (2002) we define first-order predicate calculus below. We note that the axioms 1 through 10 together with the inference rule modus ponens constitutes the propositional calculus.

Our definitions are not excately like those found on Mathworld. The reason is that we have made ⇒ right associative this means that F ⇒ G ⇒ F really means F ⇒ (G ⇒ F) below.

The [Theory pred calc] contains the following axioms

1. [pred calc rule pc1: ∀F: ∀G: F ⇒ G ⇒ F]

2. [pred calc rule pc2: ∀F: ∀G: ∀H: (F ⇒ G) ⇒ (F ⇒ G ⇒ H) ⇒ F ⇒ H]

3. [pred calc rule pc3: ∀F: ∀G: F ⇒ G ⇒ F ∧ G] 4. [pred calc rule pc4: ∀F: ∀G: F ⇒ F ∨ G]

1http://mathworld.wolfram.com/First-OrderLogic.html.

5. [pred calc rule pc5: ∀F: ∀G: F ⇒ G ∨ F]

6. [pred calc rule pc6: ∀F: ∀G: F ∧ G ⇒ F]

7. [pred calc rule pc7: ∀F: ∀G: F ∧ G ⇒ G]

8. [pred calc rule pc8: ∀F: ∀G: ∀H: (F ⇒ G) ⇒ (H ⇒ G) ⇒ F ∨ H ⇒ G]

9. [pred calc rule pc9: ∀F: ∀G: (F ⇒ G) ⇒ (F ⇒ ¬G) ⇒ ¬F]

10. [pred calc rule pc10: ∀F: ¬¬F ⇒ F]

11. [pred calc rule pc11: ∀F: ∀R: ∀X : ∀Y: Π Y.⟨F |X:= Y⟩ ⇒ ⟨F |X:= R⟩]

12. [pred calc rule pc11: ∀F: ∀R: ∀X : ∀Y: ⟨F |X:= R⟩ ⇒ Σ Y.⟨F |X:= Y⟩] We note that in first order predicate calculus metaiables used in functions

F and predicates P are object metaiables.

The only proof rule in [Theory pred calc] is Modus Ponens which says

• [pred calc rule pcmp: ∀F: ∀G: F ⊢ F ⇒ G ⊢ G]

• [pred calc rule pcia: ∀F: ∀G: ∀X : ∀Y: G ⇒ ⟨F |X:= Y⟩ ⊢ G ⇒ Π Y.⟨F |X:= Y⟩]

• [pred calc rule pcie: ∀F: ∀G: ∀X : ∀Y: ⟨F |X:= Y⟩ ⇒ G ⊢ Σ Y.⟨F |X:= Y⟩ ⇒ G]

2.1 A little proof

Below we make some small proofs just to demonstrate how to do it but also in order to test our definitions above. Lemma 2.1 [pred calc lemma trivia: ∀F: F ⇒ F]

pred calc proof of trivia:
L01: Arbitrary ≫  F  ;
L02: pc2 ≫  {(F ⇒ F ⇒ F) ⇒ (F ⇒ (F ⇒ \atop F) ⇒ F) ⇒ F ⇒ F  ;}
L03: pc1 ≫  F ⇒ F ⇒ F  ;
L04: pcmp ⊳ L03 ⊳ L02 ≫  {(F ⇒ (F ⇒ F) ⇒ F) ⇒ F ⇒ \atop F  ;}
L05: pc1 ≫  F ⇒ (F ⇒ F) ⇒ F  ;
L06: pcmp ⊳ L05 ⊳ L04 ≫  F ⇒ F  □

Lemma 2.2 [pred calc lemma iatest: ∀Y: ∀G: G ⇒ Π Y.Y ⇒ G]

pred calc proof of iatest:
L01: Arbitrary ≫  Y  ;
L02: Arbitrary ≫  G  ;
L03: pc1 ≫  G ⇒ Y ⇒ G  ;
L04: pcia ⊳ L03 ≫  G ⇒ Π Y.Y ⇒ G  □

3 First order predicate calculus

4 Zermelo-Fraenkel Axioms

Below we formally define the Zermelo-Frankel set theory. Together with the axiom of choice this is know as ZFC. Our definitions are based on those found on mathworld.wolfram.com [Theory zfc]

A Pyk definitions

([∗ ⇒ ∗ →^{pyk} “" imply "”] [pred calc →^{pyk} “pred calc”]

[pc1 →^{pyk} “pc1”]

[pc2 →^{pyk} “pc2”]

[pc3 →^{pyk} “pc3”]

[pc4 →^{pyk} “pc4”]

[pc5 →^{pyk} “pc5”]

[pc6 →^{pyk} “pc6”]

[pc7 →^{pyk} “pc7”]

[pc8 →^{pyk} “pc8”]

[pc9 →^{pyk} “pc9”]

[pc10 →^{pyk} “pc10”]

[pc11 →^{pyk} “pc11”]

[pc12 →^{pyk} “pc12”]

[pcmp →^{pyk} “pcmp”] [pcia →^{pyk} “pcia”] [pcie →^{pyk} “pcie”] [Π ∗ .∗ →^{pyk} “forall " dot "”] [Σ ∗ .∗ →^{pyk} “exists " "”]

[¬∗ →^{pyk} “lnot "”]

[∗ ∧ ∗ →^{pyk} “" land "”]

[∗ ∨ ∗ →^{pyk} “" lor "”]

[∗ ⇔ ∗ →^{pyk} “" bimply "”] [trivia →^{pyk} “trivia”] [iatest →^{pyk} “iatest”] [zfc →^{pyk} “zfc”] [test →^{pyk} “test”] )^{p}

B Tex definitions

• [¬x =^{tex} “\neg #1.”]

• [x ∧ y =^{tex} “#1. \wedge #2.”]

• [x ∨ y =^{tex} “#1. \vee #2.”]

• [x ⇒ y =^{tex} “#1. \Rightarrow #2.”]

• [x ⇔ y =^{tex} “#1. \Leftrightarrow #2.”]

• [Π y.b =^{tex} “\Pi˜ #1. . #2.”]

• [Σ y.b =^{tex} “\Sigma˜ #1. . #2.”]

C Priority table

Priority table Preassociative [test], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], ["∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗ · ∗], [∗ ·_{0} ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗], [∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗]; Preassociative [¬∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗], [∗ linebreak[4] ∗]; Preassociative [pred calc], [pc1], [pc2], [pc3], [pc4], [pc5], [pc6], [pc7], [pc8], [pc9], [pc10], [pc11], [pc12], [pcmp], [pcia], [pcie]; Postassociative [Π ∗ .∗], [Σ ∗ .∗]; Preassociative [¬∗]; Preassociative [∗ ∧ ∗]; Preassociative [∗ ∨ ∗]; Preassociative [∗ ⇔ ∗]; Preassociative [trivia], [iatest]; Preassociative [zfc]; End table