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.


Assume a cancellative semigroup (CS) admits a commutator operation, say x@y. Then the following four properties are equivalent:

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


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.

included file cs_header gt_header
theoreminput fileproofinput fileproof
(A) -> (D)AD.inAD.prf AD_gt.inAD_gt.prf
(A) -> (N)AN.inAN.prf AN_gt.inAN_gt.prf
(A) -> (E)AE.inAE.prf AE_gt.inAE_gt.prf
(D) -> (A)DA.inDA.prf DA_gt.inDA_gt.prf
(D) -> (N)DN.inDN.prf DN_gt.inDN_gt.prf
(D) -> (E)DE.inDE.prf DE_gt.inDE_gt.prf
(N) -> (A)NA.inNA.prf NA_gt.inNA_gt.prf
(N) -> (D)ND.inND.prf ND_gt.inND_gt.prf
(N) -> (E)NE.inNE.prf NE_gt.inNE_gt.prf
(E) -> (A)EA.inEA.prf EA_gt.inEA_gt.prf
(E) -> (D)ED.inED.prf ED_gt.inED_gt.prf
(E) -> (N)EN.inEN.prf EN_gt.inEN_gt.prf

Notes on the Proofs

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.) Here are the corresponding proofs in GT. 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.