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".

Introduction

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.

An Additional Theorem

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.

References

See the paper.