the class of all groups

Johan G. F. Belinfante
2008 October 18

SetDirectory["l:"];  << goedel.08oct18a; << tools.m

summary

A group is a nonempty quasigroup binary operation that is also a semigroup binary operation.  The following rewrite rule has been introduced to define the class GROUPS:

Begin["Goedel`Private`"];

FirstMatch[class[x_, member[y_, HoldPattern[GROUPS]]]]

normalization

GROUPS // Normality // Reverse

intersection[QUASIGPS, SEMIGPS, complement[set[0]]] := 
      GROUPS

The following facts are immediate consequences of the definition.

Corollary.

SubstTest[subclass, intersection[u, v], 
        u, {u -> QUASIGPS, v -> dif[SEMIGPS, set[0]]}] // 
      Reverse

subclass[GROUPS, QUASIGPS] := True

Corollary.

SubstTest[subclass, intersection[u, v], 
        v, {u -> dif[QUASIGPS, set[0]], v -> SEMIGPS}] // 
      Reverse

subclass[GROUPS, SEMIGPS] := True

Corollary.

Map[not, 
        SubstTest[subclass, intersection[u, v], 
          v, {u -> intersection[QUASIGPS, SEMIGPS], 
            v -> complement[set[0]]}]] // Reverse

member[0, GROUPS] := False

Corollary.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> GROUPS, v -> QUASIGPS, w -> BINOPS}] // 
      Reverse

subclass[GROUPS, BINOPS] := True

Corollary.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> GROUPS, v -> BINOPS, 
          w -> FUNS}] // Reverse

subclass[GROUPS, FUNS] := True

Corollary.  A group is a nonempty associative quasigroup.

AssInt[ASSOCIATIVE, BINOPS, dif[QUASIGPS, set[0]]]

intersection[ASSOCIATIVE, QUASIGPS, complement[set[0]]] := 
      GROUPS

examples

A basic example is the group of integers under addition.

SubstTest[member, INTADD, 
        intersection[u, v], {u -> SEMIGPS, 
          v -> dif[QUASIGPS, set[0]]}] // Reverse

member[INTADD, GROUPS] := True

Another collection of groups is provided by the symmetric difference operation restricted to any power set.

member[composite[SYMDIF, id[cart[P[x], P[x]]]], GROUPS] // 
      AssertTest

member[composite[SYMDIF, id[cart[P[x_], P[x_]]]], GROUPS] := 
      member[x, V]

Lemma.

Map[equal[V, class[x, #]] &, 
        SubstTest[implies, member[u, v], 
          member[range[u], 
            image[IMAGE[SECOND], v]], {u -> 
              composite[SYMDIF, id[cart[P[x], P[x]]]], v -> GROUPS}]] // 
      Reverse

subclass[range[POWER], image[IMAGE[SECOND], GROUPS]] := True

Lemma.

SubstTest[implies, member[t, V], member[range[t], V], t -> U[x]] // 
      Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.  The class of groups is not a set.

Map[and[member[GROUPS, x], #] &, 
      Map[not[implies[#, not[member[GROUPS, V]]]] &, 
        SubstTest[implies, and[subclass[u, v], member[v, V]], 
          member[u, V], {u -> range[POWER], 
            v -> image[IMAGE[SECOND], GROUPS]}]]]

member[GROUPS, x_] := False