\documentclass{amsart} \usepackage{amssymb,latexsym} \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{corollary}{Corollary} \newtheorem*{main}{Main~Theorem} \newtheorem{lemma}{Lemma} \newtheorem{proposition}{Proposition} \theoremstyle{definition} \newtheorem{definition}{Definition} \theoremstyle{remark} \newtheorem*{notation}{Notation} \numberwithin{equation}{section} \newcommand{\otter}{\textsc{Otter}} \newcommand{\sem}{\textsc{Sem}} \newcommand{\mace}{\textsc{Mace}} \newcommand{\M}{\negthinspace\wedge\negthinspace} \newcommand{\J}{\negthinspace\vee\negthinspace} \begin{document} % \sloppy \title{Yet Another Single Law for Lattices} \author{William McCune} \address{Mathematics and Computer Science Division\\ Argonne National Laboratory\\ Argonne, Illinois 60419\\ U.S.A.} \email{mccune@mcs.anl.gov} \urladdr{http://www.mcs.anl.gov/\~{}mccune} \thanks{The research of the first author was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Advanced Scientific Computing Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.} \author{R. Padmanabhan} \address{ Department of Mathematics\\ University of Manitoba\\ Winnipeg, Manitoba R3T 2N2\\ Canada} \email{padman@cc.umanitoba.ca} % \urladdr{http://www.umanitoba.ca/faculties/science/mathematics/new/faculty/html/padmanabhan.html} \urladdr{http://home.cc.umanitoba.ca/\~{}padman} \thanks{The research of the second author was supported by an operating grant from NSERC of Canada (OGP8215).} \author{Robert Veroff} \address{ Department of Computer Science\\ University of New Mexico\\ Albuquerque, New Mexico 87131\\ U.S.A.} \email{veroff@cs.unm.edu} \urladdr{http://www.cs.unm.edu/\~{}veroff} \keywords{lattice basis, lattice single identity} \subjclass{Primary: 03G10; Secondary: 06B99} \date{April 23, 2002} \begin{abstract} In this note we show that the equational theory of all lattices is defined by the single absorption law \[ (((y\J x)\M x)\J (((z\M (x\J x))\J (u\M x))\M v))\M (w\J ((s\J x)\M (x\J t))) = x. \] This identity of length 29 with 8 variables is shorter than previously known such equations defining lattices. \end{abstract} \maketitle \section{Introduction} \label{sec-intro} Given a finitely based equational theory of algebras, it is natural to determine the least number of equations needed to define that theory. Researchers have known for a long time that all finitely based group theories are one based \cite{higman-neumann}. Because of lack of a cancellation law in lattices (i.e., the absence of some kind of a subtraction operation), it was widely believed that the equational theory of lattices cannot be defined by a single identity. This belief was further strengthened by the fact that two closely related varieties, semilattices and distributive lattices, were shown to be not one based \cite{potts:1965,mckenzie-lattice}. In the late 1960s researchers attempted to formally prove that lattice theory is not one based by trying to show that no set of absorption laws valid in lattices can capture associativity. Given one such attempt \cite{mckenzie-to-rp:1968}, Padmanabhan pointed out that Sholander's 2-basis for distributive lattices \cite{sholander:lt} caused the method to collapse. This failure of the method led to a proof of existence of a single identity for lattices \cite{mckenzie-lattice}. For a partial history of various single identities defining lattices, their respective lengths, and so forth, see the latest book on lattice theory by G.~Gr\"atzer \cite[p. 477]{gratzer:1998}. In this paper we present an absorption law of length 29 with 8 variables that characterizes the equational theory of all lattices. To the best of our knowledge, the shortest previously known single identity has length 77 with 8 variables \cite{veroff:web-lt77}. Table~\ref{summary-tab} summarizes the results. \begin{table}[ht] \label{summary-tab} \small \caption{Discovery of Single Identities for Lattice Theory} \begin{tabular}{llrr} Authors & Reference & Length & Variables \\ \hline R.~McKenzie & 1970 \cite{mckenzie-lattice} & 300,000 & 34 \\ R. Padmanabhan & 1977 \cite{rp-major} & 243 & 7 \\ W. McCune, R. Padmanabhan & 1996 \cite{wwm-rp:lt-wal} & 79 & 7 \\ R. Veroff & 2001 \cite{veroff:web-lt77} & 77 & 8 \\ W. McCune, R. Padmanabhan, R. Veroff & 2002 & 29 & 8 \\ \hline \end{tabular} \end{table} \section{Methodology} The previously known single identities for lattice theory were found by procedures that take a basis in the form of absorption equations and reduce the size of the basis to a single equation. Such procedures typically produce very large equations. The single identities presented here were found by enumerating lattice identities, filtering them through sets of nonlattices, then trying to prove automatically that the surviving equations are single identities. Several programs were used. \begin{description} \item[Eq-enum] enumerates equations of the form $\alpha = x$, where $\alpha$ is in terms of meet, join, and variables. Each variable in $\alpha$, aside from $x$, has one occurrence (most-general absorption lattice identities have this property), and neither the leftmost nor the rightmost variable in $\alpha$ is $x$ (such identities are eliminated by projection models). \item[Lattice-filter] takes a stream of equations, uses Whitman's algorithm to decide which are lattice identities, and discards the nonidentities. \item[S{\small EM} \cite{sem} and M{\small ACE} \cite{mace2}] search for small, finite nonlattice models of equations. \item[Model-filter] takes a set of finite structures (nonlattices in our case) and a stream of equations and discards equations that are true in any of the structures. Most of the nonlattices were found by \sem\ or \mace; several were constructed by hand while examining candidate identities. \item[O{\small TTER} \cite{otter3}] searches for proofs of first order and equational statements. In this case, it took candidate identities and tried for several seconds to prove basic lattice properties such as commutativity, associativity, idempotence, and absorption identities. \end{description} The general method was to apply the preceding programs and incrementally build a set of nonlattice structures by using \sem\ and \mace\ to search for nonlattice models of the current candidate. Some of these structures were then added to the set and used for filtering the subsequent candidates. The programs were combined into a single program that was driven by the choice of which equations to enumerate (for example length 25 with 7 variables), and which nonlattices to use for filtering. It was run on several hundred processors, usually in jobs of 10--20 hours, over a period of several weeks. If the computation had been done on one processor, it would have taken several years. About half a trillion equations were enumerated, and the set of nonlattices grew to be several thousand, most of size 4. About 100,000 candidates survived the model filter program, and \otter\ proved basic lattice properties for several hundred of those. Further \otter\ searches on those candidates showed the following two to be single identities. \begin{equation} (((y\J x)\M x)\J (((z\M (x\J x))\J (u\M x))\M v))\M (w\J ((s\J x)\M (x\J t))) = x \tag{A1} \end{equation} \begin{equation} (((y\J x)\M x)\J (((z\M (x\J x))\J (u\M x))\M v))\M (((w\J x)\M (s\J x))\J t) = x \tag{A2} \end{equation} The first proof that (A1) is a basis took \otter\ several minutes and was more than 250 steps. The standard lattice theory 6-basis (commutativity, associativity, absorption) was derived. We then had \otter\ prove McKenzie's 4-basis (given in the next section), which produced a proof of about 170 steps in less than one minute. The 50-step proof given below was produced by Larry Wos, who used various methods to simplify \otter 's proof of the McKenzie basis. The search for single identities was not complete; that is, many shorter equations and equations with fewer variables were considered for which we could find neither countermodels nor proofs. Therefore, whether there exists a shorter single identity is an open question. \section{Proof} \label{proof-sec} McKenzie's well-known 4-basis for lattices consists of the following equations. \begin{align} x \J (y \M (x \M z)) & = x \tag{L1} \\ x \M (y \J (x \J z)) & = x \tag{L2} \\ ((y \M x) \J (x \M z)) \J x & = x \tag{L3} \\ ((y \J x) \M (x \J z)) \M x & = x \tag{L4} \end{align} The following (machine-oriented) proof is a derivation of \{L1,L2,L3,L4\} from (A1). % The justification [$i \rightarrow j$] indicates paramodulation from % $i$ into $j$, that is, unifying the left-hand side of $i$ with a % subterm of $j$, instantiating $j$ with the corresponding substitution, % and replacing the subterm with the corresponding instance of the % right-hand side of $i$. If $i$ stands for the equation $u_i=v_i$, and $j$ stands for $u_j=v_j$, then [$i\rightarrow j$] justifies an equation $u=v$ obtained in the following way. Take a subterm $s$ of $u_j$ such that $u_i$ and $s$ are unifiable by substitutions $f$ and $g$; that is, $f(u_i)$ and $g(s)$ are identical. Let $u$ be the term $g(u_j)$, but with an occurrence of $g(s)$ replaced by $f(v_i)$, and let $v$ be the term $g(v_j)$. {\small \begin{tabbing} 0000\=00000\=\kill 1 \> $(((y\J x)\M x)\J (((z\M (x\J x))\J (u\M x))\M v))\M (w\J ((s\J x)\M (x\J t)))=x$ \` [A1]\\ 2 \> $(((x\J y)\M y)\J (y\J y))\M (z\J ((u\J y)\M (y\J v)))=y$ \` [1 $\rightarrow$ 1] \\ 3 \> $(((x\J (y\J y))\M (y\J y))\J ((y\J y)\J (y\J y)))\M (z\J y)=y\J y$ \` [2 $\rightarrow$ 2] \\ 4 \> $(((x\J y)\M y)\J (((y\J y)\J (z\M y))\M u))\M (v\J ((w\J y)\M (y\J t)))=y$ \` [3 $\rightarrow$ 1] \\ 5 \> $(((x\J (((y\J y)\J (z\M y))\M u))\M (((y\J y)\J (z\M y))\M u))\J ((((y\J y)\J (z\M y))\M u)\J$ \\ \>\> $(((y\J y)\J (z\M y))\M u)))\M (v\J y)= ((y\J y)\J (z\M y))\M u$ \` [4 $\rightarrow$ 2] \\ 6 \> $(((x\J y)\M y)\J (((((y\J y)\J (z\M y))\M u)\J (v\M y))\M w))\M (t\J ((s\J y)\M (y\J r)))=y$ \` [5 $\rightarrow$ 1] \\ 7 \> $(((x\J y)\M y)\J (z\M y))\M (u\J ((v\J y)\M (y\J w)))=y$ \` [6 $\rightarrow$ 6] \\ 8 \> $(((x\J (y\M z))\M (y\M z))\J (u\M (y\M z)))\M (v\J z)=y\M z$ \` [7 $\rightarrow$ 7] \\ 9 \> $(((x\J y)\M y)\J (((z\M y)\J (u\M y))\M v))\M (w\J ((t\J y)\M (y\J s)))=y$ \` [8 $\rightarrow$ 1] \\ 10 \> $(((x\J y)\M y)\J y)\M (z\J ((u\J y)\M (y\J v)))=y$ \` [9 $\rightarrow$ 9] \\ 11 \> $(((x\J y)\M y)\J (((z\M y)\J (u\M y))\M v))\M (w\J y)=y$ \` [10 $\rightarrow$ 9] \\ 12 \> $(((x\J y)\M y)\J (z\M y))\M (u\J y)=y$ \` [10 $\rightarrow$ 7] \\ 13 \> $(((x\J y)\M y)\J (y\J y))\M (z\J y)=y$ \` [10 $\rightarrow$ 2] \\ 14 \> $(x\J (y\M (x\J x)))\M (z\J ((u\J (x\J x))\M ((x\J x)\J v)))=x\J x$ \` [13 $\rightarrow$ 7] \\ 15 \> $(x\J x)\M (y\J ((z\J (x\J x))\M ((x\J x)\J u)))=x\J x$ \` [13 $\rightarrow$ 14] \\ 16 \> $(((x\J y)\M y)\J ((z\M y)\J (z\M y)))\M (u\J y)=y$ \` [15 $\rightarrow$ 11] \\ 17 \> $((x\M y)\J (x\M y))\M (z\J y)= (x\M y)\J (x\M y)$ \` [16 $\rightarrow$ 15] \\ 18 \> $((x\J y)\M y)\J ((x\J y)\M y)=y$ \` [12 $\rightarrow$ 17] \\ 19 \> $(x\M y)\M (z\J y)=x\M y$ \` [18 $\rightarrow$ 8] \\ 20 \> $x\M (y\J x)=x$ \` [18 $\rightarrow$ 12] \\ 21 \> $x\M (y\J ((z\J x)\M (x\J u)))=x$ \` [18 $\rightarrow$ 7] \\ 22 \> $(((x\J y)\M y)\J ((z\M y)\J (u\M y)))\M (v\J y)=y$ \` [20 $\rightarrow$ 11] \\ 23 \> $((x\M y)\J (z\M y))\M (u\J y)= (x\M y)\J (z\M y)$ \` [22 $\rightarrow$ 21] \\ 24 \> $((x\J y)\M y)\J (z\M y)=y$ \` [12 $\rightarrow$ 23] \\ 25 \> $x\M (x\J y)=x$ \` [24 $\rightarrow$ 21] \\ 26 \> $((x\J y)\M y)\J ((z\M y)\J (u\M y))=y$ \` [22 $\rightarrow$ 25] \\ 27 \> $((x\J y)\M y)\J y=y$ \` [10 $\rightarrow$ 25] \\ 28 \> $x\M (y\J (x\J z))=x\M (x\J z)$ \` [25 $\rightarrow$ 19] \\ 29 \> $(x\M x)\J x=x$ \` [27 $\rightarrow$ 27] \\ 30 \> $x\M (y\J (x\M (x\J z)))=x$ \` [27 $\rightarrow$ 21] \\ 31 \> $x\M ((y\J x)\M (x\J z))=x$ \` [27 $\rightarrow$ 21] \\ 32 \> $x\M x=x$ \` [27 $\rightarrow$ 20] \\ 33 \> $x\M (y\J (x\J z))=x$ \` (L2) \ \ \ [25 $\rightarrow$ 28] \\ 34 \> $x\J x=x$ \` [32 $\rightarrow$ 29] \\ 35 \> $(x\J y)\M y=y$ \` [24 $\rightarrow$ 34] \\ 36 \> $x\M (y\M x)=y\M x$ \` [24 $\rightarrow$ 35] \\ 37 \> $(x\J (((y\M x)\J (z\M x))\M u))\M (v\J x)=x$ \` [35 $\rightarrow$ 11] \\ 38 \> $((x\J y)\M (y\J z))\M y=y\M ((x\J y)\M (y\J z))$ \` [31 $\rightarrow$ 36] \\ 39 \> $(x\J (x\M y))\M (z\J x)=x$ \` [24 $\rightarrow$ 37] \\ 40 \> $x\J (((y\M x)\J (z\M x))\M u)=x$ \` [25 $\rightarrow$ 37] \\ 41 \> $((x\J y)\M (y\J z))\M y=y$ \` (L4) \ \ \ [31 $\rightarrow$ 38] \\ 42 \> $(((x\M y)\J (z\M y))\J (((x\M y)\J (z\M y))\M u))\M y= (x\M y)\J (z\M y)$ \` [26 $\rightarrow$ 39] \\ 43 \> $(x\M y)\M x=x\M y$ \` [39 $\rightarrow$ 31] \\ 44 \> $x\J (((y\M x)\J x)\M z)=x$ \` [35 $\rightarrow$ 40] \\ 45 \> $x\J ((y\M x)\M z)=x$ \` [40 $\rightarrow$ 40] \\ 46 \> $((x\M y)\J y)\M y= (x\M y)\J y$ \` [44 $\rightarrow$ 30] \\ 47 \> $x\J (y\M (z\M x))=x$ \` [36 $\rightarrow$ 45] \\ 48 \> $(x\M y)\J y=y$ \` [35 $\rightarrow$ 46] \\ 49 \> $x\J (y\M (x\M z))=x$ \` (L1) \ \ \ [43 $\rightarrow$ 47] \\ 50 \> $((x\M y)\J (z\M y))\J y=y$ \` [42 $\rightarrow$ 48] \\ 51 \> $((x\M y)\J (y\M z))\J y=y$ \` (L3) \ \ \ [43 $\rightarrow$ 50] \\ \end{tabbing} } % end small \noindent Lines \{49,33,51,41\} are equations \{L1,L2,L3,L4\}, respectively. A similar \otter\ proof shows that (A2) is a single identity. The Web page \begin{quote} \texttt{www.mcs.anl.gov/\~{}mccune/papers/ltsax} \end{quote} contains several files associated with this note, including previously known single identities, \otter\ input files that produced the proofs, and other supporting material. \bibliographystyle{plain} % \bibliography{/home/mccune/papers/bib/master} \begin{thebibliography}{10} \bibitem{gratzer:1998} G.~{Gr\"atzer}. \newblock {\em General Lattice Theory}. \newblock Brikhauser Verlag, 2nd edition, 1998. \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{otter3} W.~McCune. \newblock Otter 3.0 {R}eference {M}anual and {G}uide. \newblock Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994. \bibitem{mace2} W.~McCune. \newblock {MACE} 2.0 {R}eference {M}anual and {G}uide. \newblock Tech. Memo ANL/MCS-TM-249, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, June 2001. \bibitem{wwm-rp:lt-wal} W.~McCune and R.~Padmanabhan. \newblock Single identities for lattice theory and for weakly associative lattices. \newblock {\em Algebra Universalis}, 36(4):436--449, 1996. \bibitem{mckenzie-to-rp:1968} R.~McKenzie, 1968. \newblock Communication to R. Padmanabhan. \bibitem{mckenzie-lattice} R.~McKenzie. \newblock Equational bases for lattice theories. \newblock {\em Math. Scand.}, 27:24--38, 1970. \bibitem{rp-major} R.~Padmanabhan. \newblock Equational theory of algebras with a majority polynomial. \newblock {\em Algebra Universalis}, 7(2):273--275, 1977. \bibitem{potts:1965} D.~H. Potts. \newblock Axioms for semi-lattices. \newblock {\em Canad. Math Bulletin}, 8:519, 1965. \bibitem{sholander:lt} M.~Sholander. \newblock Postulates for distributive lattices. \newblock {\em Canad. J. Math.}, 3:28--30, 1951. \bibitem{veroff:web-lt77} R.~Veroff. \newblock Lattice theory. \newblock http://www.cs.unm.edu/\~{}veroff/LT/, 2001. \bibitem{sem} J.~Zhang and H.~Zhang. \newblock {SEM}: A system for enumerating models. \newblock In {\em Proc. IJCAI-95}, volume~1, pages 298--303. Morgan Kaufmann, 1995. \end{thebibliography} \end{document}