Prover9 Examples: Commutators in Cancellative Semigroups

These theorems are based on the following paper.

R. Padmanabhan, W. McCune, R. Veroff, "Levi's Commutator Theorems for Cancellative Semigroups", to appear in Semigroup Forum.

In group theory, if @ is the commutator operation, the following four properties are known to be 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)

In cancellative semigroups, we cannot define the commutator operation, because we don't necessarily have in inverse operation.

Consider, however, the following property of the commutator operation.

    y * x * (x @ y) = x * y.    % CS admits commutator

Then the four properties hold for cancellative semigroups.

Here are 24 proofs. We prove all pairwise implications between the four properties for both group theory and cancellative semigroups. (Of course we only need 8 of these proofs.)

The file AD-gt.out means (A) -> (D) for group theory.

prover9 -f gt.in AD.in > AD-gt.out ; ### ( AD-gt.out.xml )

prover9 -f cs.in AD.in > AD-cs.out ; ### ( AD-cs.out.xml )

prover9 -f gt.in AE.in > AE-gt.out ; ### ( AE-gt.out.xml )

prover9 -f cs.in AE.in > AE-cs.out ; ### ( AE-cs.out.xml )

prover9 -f gt.in AN.in > AN-gt.out ; ### ( AN-gt.out.xml )

prover9 -f cs.in AN.in > AN-cs.out ; ### ( AN-cs.out.xml )

prover9 -f gt.in DA.in > DA-gt.out ; ### ( DA-gt.out.xml )

prover9 -f cs.in DA.in > DA-cs.out ; ### ( DA-cs.out.xml )

prover9 -f gt.in DE.in > DE-gt.out ; ### ( DE-gt.out.xml )

prover9 -f cs.in DE.in > DE-cs.out ; ### ( DE-cs.out.xml )

prover9 -f gt.in DN.in > DN-gt.out ; ### ( DN-gt.out.xml )

prover9 -f cs.in DN.in > DN-cs.out ; ### ( DN-cs.out.xml )

prover9 -f gt.in EA.in > EA-gt.out ; ### ( EA-gt.out.xml )

prover9 -f cs.in EA.in > EA-cs.out ; ### ( EA-cs.out.xml )

prover9 -f gt.in ED.in > ED-gt.out ; ### ( ED-gt.out.xml )

prover9 -f cs.in ED.in > ED-cs.out ; ### ( ED-cs.out.xml )

prover9 -f gt.in EN.in > EN-gt.out ; ### ( EN-gt.out.xml )

prover9 -f cs.in EN.in > EN-cs.out ; ### ( EN-cs.out.xml )

prover9 -f gt.in NA.in > NA-gt.out ; ### ( NA-gt.out.xml )

prover9 -f cs.in NA.in > NA-cs.out ; ### ( NA-cs.out.xml )

prover9 -f gt.in ND.in > ND-gt.out ; ### ( ND-gt.out.xml )

prover9 -f cs.in ND.in > ND-cs.out ; ### ( ND-cs.out.xml )

prover9 -f gt.in NE.in > NE-gt.out ; ### ( NE-gt.out.xml )

prover9 -f cs.in NE.in > NE-cs.out ; ### ( NE-cs.out.xml )