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".
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
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.
|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
x * y = u & x * z = u -> y = z % left cancellation y * x = u & z * x = u -> y = z % right cancellationwhich are different from (but equivalent to) those stated above. These forms are usually more effective in practice.
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 commutatorHere are two inputs/proofs that (A2) -> (A) in CS. (The other direction is trivial.)