\documentstyle[11pt]{article}
\textwidth=5.5in
\textheight=8.5in
\hoffset=-.25in
\voffset=-.75in
% \parskip=.1in
\newcommand{\otter}{{\sc Otter}}
\newtheorem{theorem}{Theorem}
\begin{document}
\thispagestyle{empty}
\title{\Large\bf Single Implicative Axioms for Groups\\
and for Abelian Groups}
\author{
{\it W. McCune}\thanks{
   Supported by the Mathematical, Information,
   and Computational Sciences Division subprogram of the
   Office of Computational and Technology Research,
   U.S. Department of Energy, under Contract W-31-109-Eng-38.} \\
Mathematics and Computer Science Division \\
Argonne National Laboratory \\
Argonne, Illinois  60439-4844 \\
U.S.A
%
\and
{\it A.D. Sands} \\
Department of Mathematics and Computer Science \\
University of Dundee \\
Dundee, DD1 4HN \\
Scotland \\
U.K.
%
}
\maketitle

% \section{Introduction}
Groups are usually defined by means of three axioms---the associative
law, the existence of an identity element, and the existence of an
inverse to each element.  For abelian groups, the commutative law is
included as a fourth axiom.  However, it is well known that groups
(also abelian groups) can be defined with a single equation.
In \cite{tarski-abelian-sax}, Tarski presented the single axiom
\begin{equation} \label{tarski}
x-(y-(z-(x-y))) = z
\end{equation}
for abelian groups, and in \cite{higman-neumann}, Higman and
Neumann presented the following single axiom for groups:
\begin{equation} \label{neumann}
(x/((((x/x)/y)/z)/(((x/x)/x)/z))) = y.
\end{equation}
(We use additive notation, $+$, $0$, $'$, binary $-$,
for abelian groups, and
multiplicative notation $\cdot$, $e$, ${}^{-1}$, $/$,
for ordinary groups.)

Single equational axioms in terms of product (or addition) and
inverse were first reported by Neumann in \cite{neumann-another}.  Those are
quite long with many variables, and since then, simpler ones have been
found, including
\begin{equation} \label{mccune}
((x+y)+z)+ (x+z)' = y
\end{equation}
for abelian groups \cite{sax-group}, and
\begin{equation} \label{kunen}
((z\cdot (x\cdot y)^{-1})^{-1}\cdot (z\cdot y^{-1}))\cdot
(y^{-1}\cdot y)^{-1} = x
\end{equation}
for ordinary groups \cite{kunen-sax}.

One might think it trivial, given (\ref{neumann}), to obtain a
single axiom in terms of product and inverse, by simply rewriting
$\alpha / \beta$ to $\alpha \cdot \beta^{-1}$.  Doing so gives a
single axiom, but then $\cdot$ is not product, and
$^{-1}$ is not inverse.  The same situation
holds for the abelian case.  Another curious fact is that there is no
single equational axiom for groups or for abelian groups in terms
of the three standard operations of product, inverse,
and the identity element \cite{tarski:eq}.

Three variables are required for any axiomatization of groups or of
abelian groups \cite{kunen-sax}, so (\ref{tarski}), (\ref{neumann}),
(\ref{mccune}), and (\ref{kunen}) are optimal in that respect.
With respect to length (number of symbols), (\ref{tarski}) and (\ref{mccune})
are obviously the shortest possible, (\ref{neumann}) is the shortest
known, (\ref{kunen}) is the shortest with three variables, and
the axiom \cite{sax-group}
\begin{equation}
x\cdot (y\cdot (((z\cdot z^{-1})\cdot (u\cdot y)^{-1})\cdot x))^{-1} = u,
\end{equation}
which has four variables, is the shortest possible equational axiom 
for groups in terms of product and inverse.

In this note we consider similar notions for single {\em implicative}
axioms, that is, axioms of the form $\alpha=\beta \Rightarrow \gamma=\delta$.
For abelian groups, an axiom of this type with five variables
was given by Sholander \cite{sholander-sax}.  If we allow one of
$\alpha$ and $\beta$ to be a variable, it is trivial to to obtain an
implicative axiom from an equational one: select any term $\zeta$ in the
equational axiom, replace it with a new variable $v$, and add the
antecedent $\zeta = v$.  For example, from (\ref{mccune}), we can
obtain
\begin{equation}
x+y = v\ \Rightarrow\ (v+z)+ (x+z)' = y.
\end{equation}
Hence we restrict our attention to axioms in which neither $\alpha$ nor
$\beta$ is a variable.

% \section{Implicative Axioms}
Here we present single implicative axioms for
abelian groups
in terms of addition and inverse (4 variables) and
in terms of subtraction (4 variables) and
axioms for ordinary groups
in terms of product and inverse (5 variables) and
in terms of division (4 variables).
The axioms of Theorems \ref{th:subtract} and \ref{th:ordinary} were
found and proved to be single axioms by the second author, and
those of Theorems \ref{th:abelian} and \ref{th:divide}
were found and proved to be single axioms by the
automated deduction system Otter \cite{otter3}.
All of the proofs we present are adapted from proofs found (easily) by Otter.

%------------------------------------------------- Abelian - product, inverse

\begin{theorem} \label{th:abelian}
Let $G$ be a nonempty set with binary operation $+$ and unary
operation $'$ such that for
all $x, y, z, u \in G$,
\begin{equation} \label{sax-abelian}
x + y = z + u  \ \Rightarrow\   (y'+z)+u = x
\end{equation}
Then $\langle G; +, '\rangle$ is an abelian group.
\end{theorem}

\noindent {\it Proof}.
We show the existence of an identity element, and that the inverse, 
commutativity, and associativity properties hold for $\langle G; +, '\rangle$.
First, from (\ref{sax-abelian}) we obtain
\begin{equation} \label{B1}
(y' + x) + y = x
\end{equation}
then, setting $x$ to $z+w$, and applying (\ref{sax-abelian}) again, we have
\begin{equation} \label{B2}
(y' + z) + w = y' + (z + w).
\end{equation}
(We no longer need (\ref{sax-abelian}), i.e.,
the pair (\ref{B1}) and (\ref{B2}) axiomatizes abelian groups.)
\[
\begin{array}{rcll}
a' + a & = & ((b'+a') + b) + a & \mbox{[by (\ref{B1})]} \\
       & = & (b'+(a' + b)) + a & \mbox{[by (\ref{B2})]} \\
       & = & b'+((a' + b) + a) & \mbox{[by (\ref{B2})]} \\
       & = & b'+ b.            & \mbox{[by (\ref{B1})]}
\end{array}
\]
Thus, $a' + a$ is independent of $a$, and we may call it $0$, and from
(\ref{B1}), we have that $0$ is a left identity.
\begin{eqnarray} 
x' + x  & = & 0 \label{B3} \\
0 + x  & = & x  \label{B4} 
\end{eqnarray}
Commutativity:
\[
\begin{array}{rcll}
a + b  & = & ((a' + a) + a) + b & \mbox{[by (\ref{B1})]} \\
       & = & ((b' + b) + a) + b & \mbox{[by (\ref{B3})]} \\
       & = & (b' + (b + a)) + b & \mbox{[by (\ref{B2})]} \\
       & = & b + a              & \mbox{[by (\ref{B1})]} \\

\end{array}
\]
Associativity:
\[
\begin{array}{rcll}
(a + b) + c  & = & (a + ((c' + b) + c)) + c  & \mbox{[by (\ref{B1})]} \\
             & = & (a + (c' + (b + c))) + c  & \mbox{[by (\ref{B2})]} \\
             & = & ((c' + (b + c)) + a) + c  & \mbox{[by commutativity]} \\
             & = & (c' + ((b + c) + a)) + c  & \mbox{[by (\ref{B2})]} \\
             & = & (c' + (a + (b + c))) + c  & \mbox{[by commutativity]} \\
             & = & a + (b + c)               & \mbox{[by (\ref{B1})]} \\
\end{array}
\]
Therefore, $\langle G; +, '\rangle$ is an abelian group.

%------------------------------------------------- Abelian - subtraction

\begin{theorem} \label{th:subtract}
Let $G$ be a nonempty set with a binary operation $-$ such that for
all $x, y, z, u \in G$,
\begin{equation} \label{sax-abelian-subtraction}
x-y = z-u  \ \Rightarrow\   u-(z-x) = y.
\end{equation}
Then $\langle G; -\rangle$ is an abelian group with $x-y = x + y'$
for all $x,y \in G$.
\end{theorem}

\noindent {\it Proof}.  First note that (\ref{sax-abelian-subtraction})
holds in abelian groups when $-$ is interpreted as subtraction.
The main part of the proof is to derive Tarski's axiom (\ref{tarski})
from (\ref{sax-abelian-subtraction}).
By (\ref{sax-abelian-subtraction}) we have
\begin{equation} \label{A1}
x - (y - y) = x = x - (y_1 - y_1).
\end{equation}
Applying (\ref{sax-abelian-subtraction}) to (\ref{A1}) gives us
$(y_1 - y_1) - (x - x) = y - y$,
which, by itself, yields $u - u = y - y$.
Applying (\ref{sax-abelian-subtraction}) to this, we have
\begin{equation} \label{A4}
y - (y - u) = u.
\end{equation}
Let $u$ be $v - w$, and apply (\ref{sax-abelian-subtraction})
once again to obtain
\begin{equation} \label{A5}
w - (v - y) = y - (v - w).
\end{equation}
In (\ref{A4}), let $y$ be $w$ and $u$ be $v-y$ and substitute
(\ref{A5}) to derive
\begin{equation} \label{A6}
w - (y - (v - w)) = v - y.
\end{equation}
In (\ref{A6}), let $y$ be $v$ and $u$ be $y$ and substitute
(\ref{A6}) to obtain
\[
v - (w - (y - (v - w))) = y,
\]
which is Tarski's single axiom (\ref{tarski}) for abelian groups in terms
of subtraction.

% ------------------------------------------------- Ordinary - product, inverse

\begin{theorem} \label{th:ordinary}
Let $G$ be a nonempty set with binary operation $\cdot$ and unary
operation ${}^{-1}$ such that for
all $x, y, z, u \in G$,
\begin{equation} \label{sax}
(x\cdot y)\cdot z = (x\cdot u)\cdot w  \ \Rightarrow\
u\cdot (w\cdot z^{-1}) = y
\end{equation}
Then $\langle G; \cdot, {}^{-1}\rangle$ is a group.
\end{theorem}

\noindent {\it Proof}.
By (\ref{sax}) we have $x \cdot (y \cdot y^{-1})=x=x \cdot (z \cdot z^{-1})$;
hence $(x \cdot (y \cdot y^{-1})) \cdot u=(x \cdot (z \cdot z^{-1})) \cdot u$;
hence by (\ref{sax}),
$(z \cdot z^{-1}) \cdot (u \cdot u^{-1})=(y \cdot y^{-1})$;
hence $y \cdot y^{-1}$ is independent of $y$,
and we name the element $e$, which is a right identity,
\begin{equation} 
y  \cdot  y^{-1} = e,  \label{D2}
\end{equation}
\begin{equation} 
x  \cdot  e =  x.  \label{D3} 
\end{equation}
We have $(e \cdot e) \cdot e=(e \cdot e^{-1}) \cdot e$,
and by (\ref{sax}), $e^{-1} \cdot (e \cdot e^{-1})=e$, hence
\begin{equation} \label{D4}
e^{-1}=e.
\end{equation}
Next, we have $(e \cdot x) \cdot e=(e \cdot e) \cdot x$,
and by (\ref{sax}), $e \cdot (x \cdot e^{-1})=x$, hence
\begin{equation} \label{D5}
e \cdot x=x.
\end{equation}
Now, we have $(e \cdot x) \cdot y=(e \cdot (x \cdot y)) \cdot e$,
and by (\ref{sax}), $(x \cdot y) \cdot (e \cdot y^{-1})=x$, hence
\begin{equation} \label{D6}
(x \cdot y) \cdot y^{-1}=x.
\end{equation}
Finally, by (\ref{D5}) and (\ref{D6}),
we have $(e \cdot ((x \cdot y) \cdot z)) \cdot z^{-1}=(e \cdot x) \cdot y$,
and by (\ref{sax}),
$x \cdot (y \cdot z^{-1}{}^{-1}) = (x \cdot y) \cdot z$, and by (\ref{D6}),
$x \cdot ( ((y \cdot z) \cdot z^{-1}) \cdot z^{-1}{}^{-1}) =
(x \cdot y) \cdot z$,
and by (\ref{D6}) again,
\begin{equation} \label{D7}
x \cdot (y \cdot z) = (x \cdot y) \cdot z.
\end{equation}
Equations (\ref{D2}), (\ref{D3}), and (\ref{D7}) establish the result.

% ------------------------------------------------- Ordinary - division

The proof of the following theorem is in the form produced by the
theorem prover Otter.  The justification $m\rightarrow n$ indicates
substitution of an instance of the right side of equation $m$ for an
instance of a term in the left side of $n$, and $:i,j,\cdots$
indicates simplification with $i, j, \cdots$.
Variables are automatically renamed by the program, and the numbering
of the equations reflects the sequence of equations retained by the
program.

\begin{theorem} \label{th:divide}
Let $G$ be a nonempty set with a binary operation $/$ such that for
all $x, y, z, u \in G$,
\begin{equation} \label{sax-division}
x/y=z/u  \ \Rightarrow\   y/(((z/z)/z)/((x/x)/x))=u
\end{equation}
Then $\langle G; /\rangle$ is a group with $x/y = x \cdot y^{-1}$
for all $x,y \in G$.
\end{theorem}

\noindent {\it Proof}.
First Otter shows that $x/x$ is independent of $x$.
Terms of the form $(v/v)/v$ are abbreviated as $f(v)$.
\begin{tabbing}
\=00000000\=\kill
\> 2 \> $x=x$  \\
\> 3 \> $x/y = z/u \ \rightarrow\ y/ (f(z)/ f(x))=u$  \\[.2cm]
\> 5 \> $x/ (f(y)/ f(y))=x$ \` [3,2] \\
\> 6 \> $(f(x)/ f(x))/ (f(y)/ (((y/z)/ (y/z))/ (y/z)))=z$ \` [3,5] \\
\> 10 \> $f(x)/ f(x)= f(y)/ f(y)$ \` [5 $\rightarrow$ 6 :5,5,5] \\
\> 11 \> $(f(x)/ f(x))/ ((f(y)/ f(y))/ f(y))= f(y)$ \` [5 $\rightarrow$ 6 :5,5] \\
\> 19 \> $(f(x)/ f(x))/ ((((y/y)/ (y/y))/ (y/y))/ ((f(z)/ f(z))/ f(y)))=y$ \` [10 $\rightarrow$ 6] \\
\> 22 \> $x/ (((f(y)/ f(y))/ f(z))/ ((f(z)/ f(z))/ f(z)))=x$ \` [10 $\rightarrow$ 5] \\
\> 25 \> $(f(x)/ f(x))/ ((f(y)/ f(y))/ f(z))= f(z)$ \` [10 $\rightarrow$ 11] \\
\> 29 \> $(((x/x)/ (x/x))/ (x/x))/ ((f(y)/ f(y))/ f(x))= f(x)$ \` [18 $\rightarrow$ 6 :5,5,19,19,25] \\
\> 31 \> $(f(x)/ f(x))/ f(y)=y$ \` [19 :29] \\
\> 36 \> $x/ (y/y)=x$ \` [22 :31,31] \\
\> 40 \> $(x/x)/ f(y)=y$ \` [10 $\rightarrow$ 31 :31,31] \\
\> 54 \> $x/x=y/y$ \` [36 $\rightarrow$ 40 :36,36]
\end{tabbing}
We now introduce the element $e$ and use $x / x = e$
to prove the Higman-Neumann single axiom (\ref{neumann}).
We assert that there are elements $A$, $B$, and $C$ for which (\ref{neumann})
fails to hold and Otter derives a contradiction.
\begin{tabbing}
\=00000000\=\kill
\> 1 \> $x=x$  \\
\> 2 \> $x/y = z/u \ \rightarrow\ y/ (((z/z)/z)/ ((x/x)/x))=u$  \\
\> 4 \> $x/x=e$  \\
\> 5 \> $A/ ((((A/A)/B)/C)/ (((A/A)/A)/C)) \neq B$  \\[.2cm]
\> 6 \> $A/ (((e/B)/C)/ ((e/A)/C)) \neq B$ \` [5 :4,4] \\
\> 7 \> $x/y = z/u \ \rightarrow\ y/ ((e/z)/ (e/x))=u$ \` [2 :4,4] \\
\> 9 \> $x/e=x$ \` [7,1 :4] \\
\> 10 \> $e/ ((e/x)/ (e/ (x/y)))=y$ \` [7,9] \\
\> 12 \> $((e/x)/ (e/ (x/ (y/z))))/ (e/y)=z$ \` [7,10 :4,9] \\
\> 17 \> $(e/x)/ (e/ (x/y))=e/ (e/ (e/y))$ \` [10 $\rightarrow$ 10 :4] \\
\> 19 \> $e/ (e/x)=x$ \` [4 $\rightarrow$ 10 :4,9] \\
\> 20 \> $(e/ (x/y))/ (e/x)=y$ \` [12 :17,19] \\
\> 24 \> $(e/x)/ ((e/y)/ (x/ (y/z)))=z$ \` [7,20 :19] \\
\> 28 \> $(e/ ((e/x)/y))/x=y$ \` [19 $\rightarrow$ 20] \\
\> 30 \> $x/ ((e/y)/ ((e/x)/ (y/z)))=z$ \` [19 $\rightarrow$ 24] \\
\> 103 \> $x/ (((e/y)/z)/ ((e/x)/z))=y$ \` [28 $\rightarrow$ 30 :19] \\
\> 105 \> $\Box$ \` [103,6]
\end{tabbing}
Because (\ref{sax-division}) holds for groups when $/$ is interpreted
as division, and because the Higman-Neumann axiom can be derived,
the proof is complete.

% ------------------------------------------------- end of theorems

The main open question remaining is whether there exists a
four-variable single implicative axiom in terms of product and inverse
for ordinary groups.  Also, for the non-abelian cases, we do not know
if there exist implicative axioms shorter than ours.

Each of the four proofs we have presented arises from a different
amount of translation (by hand) from the Otter-generated proof, and
each is in a different style.  The proof of Theorem \ref{th:abelian}
has had the most translation and is probably the most transparent
(also it is the easiest theorem).  Theorem \ref{th:divide}'s proof is
nearly in the form produced by Otter and is probably opaque to most
readers (it certainly is to us).  Translating proofs found by
computers into human-readable forms is an important problem in
automated deduction.

The Otter input files and proofs for these four theorems are
available on the World Wide Web
through \verb|http://www.mcs.anl.gov/home/mccune/ar/imply/|.

\bibliographystyle{plain}

\begin{thebibliography}{1}

\bibitem{higman-neumann}
G.~Higman and B.~H. Neumann.
\newblock Groups as groupoids with one law.
\newblock {\em Publicationes Mathematicae Debrecen}, 2:215--227, 1952.

\bibitem{kunen-sax}
K.~Kunen.
\newblock Single axioms for groups.
\newblock {\em Journal of Automated Reasoning}, 9(3):291--308, 1992.

\bibitem{sax-group}
W.~McCune.
\newblock Single axioms for groups and {A}belian groups with various
  operations.
\newblock {\em Journal of Automated Reasoning}, 10(1):1--13, 1993.

\bibitem{otter3}
W.~McCune.
\newblock {\sc Otter} 3.0 {R}eference {M}anual and {G}uide.
\newblock Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL,
  1994.  See also \verb|http://www.mcs.anl.gov/home/mccune/ar/otter/|.

\bibitem{neumann-another}
B.~H. Neumann.
\newblock Another single law for groups.
\newblock {\em Bull. Australian Math. Soc.}, 23:81--102, 1981.

\bibitem{sholander-sax}
M.~Sholander.
\newblock Postulates for commutative groups.
\newblock {\em Amer. Math. Monthly}, 66:93--95, 1959.

\bibitem{tarski-abelian-sax}
A.~Tarski.
\newblock Ein {B}eitrag zur {A}xiomatik der {A}belschen {G}ruppen.
\newblock {\em Fundamenta Mathematicae}, 30:253--256, 1938.

\bibitem{tarski:eq}
A.~Tarski.
\newblock Equational logic and equational theories of algebras.
\newblock In K.~{Sch\"utte}, editor, {\em Contributions to Mathematical Logic},
  pages 275--288. North-Holland, Amsterdam, 1968.

\end{thebibliography}

\end{document}

