\documentclass{article}

\usepackage{amsmath}
\usepackage{amssymb}

\begin{document}  \sloppy

\title{\Large\textbf{Levi's Commutator Theorems\\for Cancellative Semigroups}}

\author{
  \textbf{R. Padmanabhan\thanks
    {
      Supported by an operating grant from NSERC of Canada (OGP8215).
  }}
  \and
  \textbf{W. McCune\thanks
    {
      Supported by the Mathematical, Information, and Computational  
      Sciences Division subprogram of the Office of Advanced Scientific
      Computing  Research, Office of Science, U.S. Department of
      Energy, under Contract W-31-109-ENG-38.
  }}
  \and
  \textbf{R. Veroff\thanks{
      Supported by the U.S. National Science Foundation
      grant CDA-9503064.
  }}
}

\date{}

\maketitle

\begin{abstract}
\noindent
A conjecture of Padmanabhan, on provability in cancellative semigroups,
is addressed.  Several of Levi's group theory commutator theorems 
are proved for cancellative semigroups.  The proofs, found by
automated deduction, support the conjecture.

\medskip
\noindent\small\textbf{Key words and phrases}:
cancellative semigroup, commutator, automated theorem proving.

\medskip
\noindent\small\textbf{2000 Mathematics Subject Classification}:
20M07, 20A05, 68T15.
\end{abstract}

\section{Introduction} \label{sec-intro}

The following conjecture (apparently still open) was formulated
by the first author in the 1980s and published
in \cite{wm-rp:monograph}.

{\em Conjecture.}  Let $\Sigma$ be a nonempty set of equations of type
$\langle 2\rangle$, and let $\sigma$ be an equation of the same type.  If
every group satisfying $\Sigma$ also satisfies $\sigma$,
then every cancellative
semigroup satisfying $\Sigma$ must satisfy $\sigma$ as well.  To put it more
formally, let GT be the axioms of group theory and CS be the
axioms for cancellative semigroups, that is,
the associative law and the two cancellation laws.  Then
\begin{equation*}
\mbox{if}\ (\Sigma, \mbox{GT} \Rightarrow \sigma),\
\mbox{then}\ (\Sigma, \mbox{CS} \Rightarrow \sigma).
\end{equation*}
From the deductive point of view, this conjecture says that if one
uses the richer language of group theory (i.e., with inverse and identity)
to derive $\sigma$ from $\Sigma$, then one can do the same thing within the
limited language of just one binary operation that is associative and
cancellative.

For example, the statement
\begin{equation*}
xyzyx = yxzxy\ \ \Rightarrow\ \ xyyx = yxxy.
\end{equation*}
supports the conjecture.  It satisfies the conditions of the
conjecture, it has a proof in GT (trivial, by letting $z$ be
the identity), and the following proof shows it to hold for CS.
\begin{equation*}
\begin{split}
(xyyx)(xyx) &= (xy)(yxx)(yx)\\
            &= (yx)(yxx)(xy)\ \ \mbox{[by the assumed identity with $z = xyx$]}\\
            &= (yx)(yx)x(xy)\\
            &= (yx)(xy)x(yx)\ \ \mbox{[by the assumed identity with $z = x$]}\\
            &= (yxxy)(xyx)\\
       xyyx &= yxxy\ \ \mbox{[by canceling $(xyx)$]}\ \ \Box
\end{split}
\end{equation*}
\noindent
Unfortunately, the proof in GT does not seem to tell us much
about how to prove it in CS.  
Many such examples supporting the conjecture can be found
in \cite{wm-rp:monograph}.

Here we do not directly address the conjecture; rather, we
provide further intuitive support for it by considering several theorems
about commutators in GT and the corresponding statements in CS.
Automated theorem proving was used to find proofs for the GT and the
CS theorems.
Apart from being generalizations,
these proofs are strictly first order
(e.g., avoiding quotient constructions) and
hence may be construed as providing new equational proofs of the 
well known theorems in GT.

\section{Commutator Theorems in GT and in CS}

In GT, let the commutator operation be defined as
\begin{equation}
[x,y] = x^{-1} y^{-1} x y.  \tag{C1} 
\end{equation}
The following three statements about commutators,
\begin{alignat}{2}
[x,y] z   & = z [x,y]     & \qquad & \mbox{(nilpotency of class 2)} \tag{N} \\
[[x,y],z] & = [u,[v,w]]   & \qquad & \mbox{(``associativity'' of commutator)} \tag{A} \\
[xy,z]    & = [x,z] [y,z] & \qquad & \mbox{(distributivity)},       \tag{D}
\end{alignat}
are well known to be equivalent in GT \cite[p. 99]{kurosh}.
We refer to this fact as Levi's theorem on commutators.
See the Web page \cite{cs-web} for equational proofs found by
a theorem-proving program.

Consider the analogous problem in CS.
We cannot use (C1) to define the commutator because
the inverse operation is not in the language.
Instead, we simply state the following property of the new operation:
\begin{equation}
y x [x,y] = x y.  \tag{C2}
\end{equation}
Indeed, such an element $[x,y]$ is unique by the cancellation law.

In the following section, we show informally that given (C2), the
equations (N), (A), and (D) are equivalent in CS.  In group theory,
these three properties are equivalent to the group being nilpotent of
class 2.  This is the essence of Levi's theorem on commutators.
Thus, to capture the full scenario of Levi, we need to define the
concept of nilpotence class 2 in a manner meaningful in CS,
that is, with no mention of the inverse operation.
This is precisely the role played by the identity
\begin{alignat}{2}
xyzyx       & = yxzxy.  & \qquad & \mbox{(CS essence of (N))} \tag{E}
\end{alignat}
This was first discovered by A.~I.~Malcev in \cite{malcev:cs}.
In fact, he proved that any cancellative semigroup
satisfying the property (E) is embeddable in a group
of nilpotence class 2.

Note that these equations are outside the hypotheses of the conjecture
on cancellative semigroups.  First, there is an additional operation.
Second, the CS versions use property (C2) instead of the
definition (C1), giving slightly stronger theorems (which hold
obviously for GT as well).  Also, if a cancellative semigroup
satisfies (C2), there is a
left and right identity element for the semigroup operation (see
Section \ref{sec-auto}), which allows the CS proofs to be a bit more
grouplike.

\section{Proof Sketch}

By Malcev's discovery, the class of all
cancellative semigroups satisfying (E) is identical to the class of all
subsemigroups of nilpotent groups of class 2.  Combining this with the
proofs given by Kurosh of Levi's theorems on commutators 
\cite[p. 91]{kurosh}, we have a model-theoretic proof
that property (E) is equivalent to
(N), (A), and (D) in the class of all cancellative semigroups.

By the completeness theorem of first-order logic with equality,
there must be proofs of this equivalence within the first-order
theory of CS.
The automated theorem-proving program Otter \cite{otter33} has
found such proofs, and we show one of the longer proofs in
the following section.  The other Otter proofs showing all of
the equivalences can be found on the Web page associated
with this paper \cite{cs-web}.

\section{Computer Proof of $(E) \Rightarrow (D)$}  \label{sec-auto}

Here we give a formal equational proof that property (E) implies
the distributivity property (D) in CS.  The proof
was found by Otter.  (Notes on the proofs are given below.)
First, Otter shows the existence of a constant $[x,x]$.

\begin{tabbing} 0000000\=\kill
2 \> $x=x$ \` [] \\
3 \> $x y = z,\ x u = z \rightarrow y=u$ \` [left cancellation] \\
4 \> $x y = z,\ u y = z \rightarrow x=u$ \` [right cancellation] \\
5 \> $(x y) z=x y z$ \` [associativity of $\cdot$] \\
7 \> $x y [y,x]=y x$ \` [commutator property] \\[.25cm]
11 \> $x [x,x]=x$ \` [3,2,7] \\
21 \> $x [x,x] y=x y$ \` [11 $\rightarrow$ 5] \\
31 \> $[x,x] y=y$ \` [3,2,21] \\
33 \> $[x,x]=[y,y]$ \` [4,31,31]
\end{tabbing}
Now Otter proves that (E) $\Rightarrow$ (D) in CS.

\begin{tabbing} 0000000\=\kill
2 \> $x=x$ \` [] \\
3 \> $x y = z,\ x u = z \rightarrow y=u$ \` [left cancellation] \\
4 \> $x y = z,\ u y = z \rightarrow x=u$ \` [right cancellation] \\
5 \> $(x y) z=x y z$ \` [associativity of .] \\
7 \> $x y [y,x]=y x$ \` [commutator property] \\
10 \> $x y z y x=y x z x y$ \` [property (E)] \\
11 \> $[x,x]=e$ \` [constant e] \\[.25cm]
15 \> $x e=x$ \` [3,2,7:11] \\
17 \> $x y z [y z,x]=y z x$ \` [5 $\rightarrow$ 7:5] \\
19 \> $x y z [z,x y]=z x y$ \` [5 $\rightarrow$ 7] \\
21 \> $x y [y,x] z=y x z$ \` [7 $\rightarrow$ 5:5,5] \\
24 \> $x e y=x y$ \` [15 $\rightarrow$ 5] \\
30 \> $x y [x y,x]=y x$ \` [3,2,17] \\
36 \> $e x=x$ \` [3,7,24:11,15] \\
39 \> $x y [y,y x]=y x$ \` [3,2,19] \\
44 \> $x [x,e]=x$ \` [3,7,36:15] \\
49 \> $x [e,x]=x$ \` [36 $\rightarrow$ 7:36] \\
51 \> $[x,e]=e$ \` [3,15,44] \\
56 \> $x y x z=x [x,z] y z x$ \` [3,10,21] \\
57 \> $x [x,y] z=z x [x,y z]$ \` [3,21,19] \\
63 \> $[x,y] y x=x y [[x,y],y x]$ \` [19 $\rightarrow$ 21] \\
65 \> $[e,x]=e$ \` [3,15,49] \\
67 \> $x [y x,y]=x [x,y]$ \` [3,7,30] \\
75 \> $x [x,x y]=x [x,y]$ \` [3,7,39] \\
77 \> $[x y,x]=[y,x]$ \` [3,2,67] \\
89 \> $[x y z,x y]=[z,x y]$ \` [5 $\rightarrow$ 77] \\
91 \> $[x,x y]=[x,y]$ \` [3,2,75] \\
111 \> $[x y,x y z]=[x y,z]$ \` [5 $\rightarrow$ 91] \\
151 \> $[x y,y x]=[[x,y],y x]$ \` [7 $\rightarrow$ 89] \\
156 \> $[x,y] z y x=z x y$ \` [3,2,56] \\
157 \> $x y z=[y,z] x z y$ \` [3,56,2] \\
158 \> $[x,[x,y] z y x]=[x,z x y]$ \` [56 $\rightarrow$ 91:91] \\
160 \> $[x,y x z]=[x,[x,z] y z x]$ \` [158] \\
167 \> $[[x,y],y x]=[x y,[y,x]]$ \` [7 $\rightarrow$ 111:151] \\
169 \> $[x y,[y,x]]=[[x,y],y x]$ \` [167] \\
170 \> $x [x,y] [y,z x]=[y,z] x$ \` [3,21,57] \\
180 \> $x y [[x,y],y x]=x y$ \` [3,2,156:63] \\
182 \> $[x,y] y x=x y$ \` [63:180] \\
196 \> $[[x,y],z x y]=[[x,y],z y x]$ \` [156 $\rightarrow$ 91] \\
210 \> $[x,y z] y z x=x y z$ \` [5 $\rightarrow$ 182] \\
225 \> $[x y,[x,y]]=[y x,[x,y]]$ \` [182 $\rightarrow$ 77] \\
226 \> $[x,y] y x z=x y z$ \` [182 $\rightarrow$ 5:5,5] \\
229 \> $[x y,[y,x]]=[y x,[y,x]]$ \` [225] \\
280 \> $x y [[x,y],z y x]=x y$ \` [3,19,157:5,21] \\
286 \> $[x,y z] z y x=x z y$ \` [156 $\rightarrow$ 157:5,226] \\
384 \> $x [[y,x],x y]=x$ \` [3,2,180] \\
387 \> $[[x,y],y x]=e$ \` [3,15,384] \\
391 \> $[x y,[y,x]]=e$ \` [169:387] \\
399 \> $[x y,[x,y]]=e$ \` [229:391] \\
1669 \> $[x,y] [y,z x]=[y,z] [[y,z],x]$ \` [3,170,7] \\
1670 \> $x [x,y] [y,x]=x$ \` [36 $\rightarrow$ 170:51,36] \\
1755 \> $[x,y] [y,x]=e$ \` [3,15,1670] \\
1797 \> $[x,y] [y,x] z=z$ \` [1755 $\rightarrow$ 17:65,15,1755,15] \\
1998 \> $[[x,y],z] [y,x] z [x,y]=z$ \` [157 $\rightarrow$ 1797] \\
2689 \> $[[x,y],z] x y=x y$ \` [196 $\rightarrow$ 170:399,36,5,280] \\
3280 \> $[x,y z]=[x,z y]$ \` [4,210,286] \\
3373 \> $[x,[y,z] u z y]=[x,y z u]$ \` [157 $\rightarrow$ 3280:5] \\
3428 \> $[x,y x z]=[x,z y]$ \` [160:3373,91] \\
3429 \> $[x,y z]=[x,z x y]$ \` [158:3373,91] \\
5622 \> $[[x,y],z]=e$ \` [4,36,2689] \\
5644 \> $[x,y] z [y,x]=z$ \` [1998:5622,36] \\
5646 \> $[x,y] [y,z x]=[y,z]$ \` [1669:5622,15] \\
5968 \> $[x,y x z]=[x,y z]$ \` [3428 $\rightarrow$ 3429:5,91] \\
6186 \> $[x,y] [x,z]=[x,y z]$ \` [3,5644,5646] \\
6243 \> $[x,y z] [z,y x]=[x z,y]$ \` [89 $\rightarrow$ 5646:5968,77] \\
6516 \> $[x,y z] u=[x,y] [x,z] u$ \` [6186 $\rightarrow$ 5] \\
6522 \> $[x,y] [z,y]=[x z,y]$\ \ (property (D)) \` [6243:6516,5646] \ \ $\Box$
\end{tabbing}

In the preceding proof, the justification $i \rightarrow j$ indicates
equality substitution between an instance of $i$ and an instance of $j$,
and the justification $:i,j,\ldots$ indicates simplification with
$i,j,\ldots$.

The proof, found by Otter in several seconds, is in nearly the
form output by Otter, and there is much room for improvement
of the presentation.  Inferences are frequently hard to follow,
because the instances of the premises are not given, simplification
is applied, and variables are renamed.  In addition,
Otter proofs are usually longer than necessary.

Otter can accept various forms and degrees of guidance from
the user when searching for a proof.  For these proofs, we
simply specified an ordering on the symbols (which affects how
derived identities are used as simplification rules) and
a limit on the complexity of derived identities.

Automated theorem proving has been very useful in testing other instances
of the CS conjecture \cite{wm-rp:monograph}, and we are using
the resulting proofs to seek insights into the relationships between
CS proofs and the corresponding GT proofs.

\bibliographystyle{plain}

% \bibliography{/home/mccune/papers/bib/master}

\begin{thebibliography}{1}

\bibitem{kurosh}
A.~G. Kurosh.
\newblock {\em The Theory of Groups}, Volume~1.
\newblock Chelsea, New York, 1956.

\bibitem{malcev:cs}
A.~I. Malcev.
\newblock Nilpotent semigroups.
\newblock {\em Ivanov. Gos. Ped. Inst. Zap. Fiz.-Mat. Nauki}, 4:107--111, 1953.
\newblock In Russian.

\bibitem{otter33}
W.~McCune.
\newblock Otter 3.3 {R}eference {M}anual.
\newblock Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division,
  Argonne National Laboratory, Argonne, IL, August 2003.

\bibitem{wm-rp:monograph}
W.~McCune and R.~Padmanabhan.
\newblock {\em Automated Deduction in Equational Logic and Cubic Curves},
  volume 1095 of {\em Lecture Notes in Computer Science (AI subseries)}.
\newblock Springer-Verlag, Berlin, 1996.

\bibitem{cs-web}
R.~Padmanabhan, W.~McCune, and R.~Veroff.
\newblock Levi's commutator theorems for cancellative semigroups: Web support.
\newblock \verb|http://www.mcs.anl.gov/~mccune/papers/cs-commutator/|, 2003.

\end{thebibliography}

\bigskip

{\small

\begin{verse}
% R. Padmanabhan\\
Department of Mathematics\\
University of Manitoba\\
Winnipeg, Manitoba  R3T 2N2, Canada\\
padman@cc.umanitoba.ca
\end{verse}

\begin{verse}
% William McCune\\
Mathematics and Computer Science Division\\
Argonne National Laboratory\\
Argonne, Illinois  60419, USA\\
mccune@mcs.anl.gov
\end{verse}

\begin{verse}
% Robert Veroff\\
Department of Computer Science\\
University of New Mexico\\
Albuquerque, New Mexico  87131, USA\\
veroff@cs.unm.edu
\end{verse}

}

\end{document}
