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