# Levi's Commutator Theorems for Cancellative Semigroups: Web Support

R. Padmanabhan, William McCune, Robert Veroff

This web page supports a paper accepted for publication in Semigroup Forum.

Here is the final version for the publisher (February 1, 2005).

Son of BirdBrain, the Web-based demo of Otter and Mace2, can prove many of the easy theorems cited in the paper. Try it now --- select the area "CS commutator".

See the paper.

## Theorem

Assume a cancellative semigroup (CS) admits a commutator operation, say x@y. Then the following four properties are equivalent:
• (A) the commutator operation is "associative" (actually, the property we use is much more general than associativity);
• (N) the semigroup is nilpotent of class 2;
• (D) commutator distributes over product.
• (E) cancellative semigroup essence of property (N);

That is, given the statements

```    (x * y) * z = x * (y * z)          (S) * is a semigroup
x * y = x * z  ->  y = z           (LC) left cancellation for *
y * x = z * x  ->  y = z           (RC) right cancellation for *
x * y = y * x * (x @ y)            (C) * admits a commutator operation @
```
the following four properties are (pairwise) equivalent.
```    (x @ y) @ z = u @ (v @ w)          (A) "associativity" of commutator
(x @ y) * z = z * (x @ y)          (N) nilpotency of class 2
(x * y) @ z = (x @ z) * (y @ z)    (D) distributivity of commutator
x*y*z*y*x = y*x*z*x*y              (E) CS essence of (N)
```
This is a generalization of the corresponding theorem for group theory, in which the commutator operation is defined as
```    x @ y = i(x) * i(y) * x * y
```

## Proofs

First we show that cancellative semigroups admitting a commutator operation, as stated above, have a constant x @ x which is a left and right identity for the semigroup operation (input, proof). This allows us to include the equations (e is a constant)
```    x @ x = e.
x * e = x.
e * x = x.
```
for the CS proofs below.

Here are 12 Otter proofs for CS. For each of the four properties, the other three are derived. (Of course we only need a four-cycle of these.) Also included are the corresponding theorems for GT.

 CS GT included file cs_header gt_header theorem input file proof input file proof (A) -> (D) AD.in AD.prf AD_gt.in AD_gt.prf (A) -> (N) AN.in AN.prf AN_gt.in AN_gt.prf (A) -> (E) AE.in AE.prf AE_gt.in AE_gt.prf (D) -> (A) DA.in DA.prf DA_gt.in DA_gt.prf (D) -> (N) DN.in DN.prf DN_gt.in DN_gt.prf (D) -> (E) DE.in DE.prf DE_gt.in DE_gt.prf (N) -> (A) NA.in NA.prf NA_gt.in NA_gt.prf (N) -> (D) ND.in ND.prf ND_gt.in ND_gt.prf (N) -> (E) NE.in NE.prf NE_gt.in NE_gt.prf (E) -> (A) EA.in EA.prf EA_gt.in EA_gt.prf (E) -> (D) ED.in ED.prf ED_gt.in ED_gt.prf (E) -> (N) EN.in EN.prf EN_gt.in EN_gt.prf

Notes on the Proofs

• All 12 CS input files specify the same search strategy and parameters, given in the file cs_header which is included by each of the 12 input files. We arrived at these settings by experimentation. Similarly, the 12 GT input files include the file gt_header
• We use the following forms of the cancellation laws,
```    x * y = u  &  x * z = u  ->  y = z   % left cancellation
y * x = u  &  z * x = u  ->  y = z   % right cancellation
```
which are different from (but equivalent to) those stated above. These forms are usually more effective in practice.
• The proofs are probably much longer than necessary (Otter is like that). We have not yet tried to shorten them.

A fifth property equivalent to the others is ordinary associativity of the commutator operation:

```    (x @ y) @ z = x @ (y @ z)          (A2) true associativity of commutator
```
Here are two inputs/proofs that (A2) -> (A) in CS. (The other direction is trivial.)
• assoc.in, assoc.prf. This search uses the same CS strategy as above. It takes a long time and produces a long proof.
• assoc-b.in, assoc-b.prf. For this search we have added a weighting strategy to delete equations containing specified patterns of terms. This takes only a few seconds and produces a much better proof.
Here are the corresponding proofs in GT.
• assoc-gt.in, assoc-gt.prf. This search uses the same CS strategy as above. It takes a long time and produces a long proof.
• assoc-gt-b.in, assoc-gt-b.prf. For this search we have added a weighting strategy to delete equations containing specified patterns of terms. This takes only a few seconds and produces a much better proof.
Note to the authors: should we have used this version of associativity in the main section of the paper? Kurosh uses it for the GT proofs.

See the paper.