\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Group Theory - HOL

Table of Contents

1. Introduction

The basic idea is that set membership \(x\in A\) is modeled by the predicate \(\mathtt{InA}[x] := x\in A\). We then blur this distinction, and just consider a set to be a HOL term with signature \(A\colon\ast\to\mathrm{bool}\).

Then a group is a pair \((G,*)\) satisfying a bunch of properties. The definition we will formalize is:

A Group consists of a set \(G\) and a binary operator \(\mathtt{prod}\) such that

  1. for every pair of elements \(x,y\in G\), the element \(\mathtt{prod}~x~y~\in G\) (so \(G\) is closed under \(\mathtt{prod}\))
  2. For every \(x,y,z\in G\) we have \(\mathtt{prod}~(\mathtt{prod}~x~y)~z=\mathtt{prod}~x~(\mathtt{prod}~y~z)\)
  3. There exists an element \(e\in G\) such that:
    1. for every \(x\in G\), we have \(\mathtt{prod}~e~x=x\) (i.e., \(e\) is a left identity element for prod)
    2. For every \(x\in G\), there exists a \(y\in G\) such that \(\mathtt{prod}~y~x=e\) (i.e., \(G\) has left inverses with respect to \(e\)).

Everything else may be derived from these axioms. 

GROUP-DEF =
|- !G prod.
   GROUP(G,prod)=
   (!x y. G x /\ G y ==> G(prod x y)) /\
   (!x y z. G x /\ G y /\ G z ==> (prod(prod x y)z = prod x(prod y z ))) /\
   (?e.
     G e /\
     (!x. G x ==> (prod e x = x)) /\
     (!x. G x ==> (?y. G y /\ (prod y x = e))))

2. References

  • Elsa L. Gunter,
    "Doing Algebra in Simple Type Theory".
    U. Pennsylvania, Tech. Report No. MS-CIS-89-38, June 1989. Eprint, 44 pages.

Last Updated 2022-04-30 Sat 08:33.