This is joint work with Bill McCune and R. Padmanabhan.
McCune and Padmanabhan present (Theorem LT-12 on page 144 of [2]) the following single equational axiom for lattice theory.
(((x ^ y) v (y ^ (x v y))) ^ z) v (((x ^ (((x1 ^ y) v (y ^ x2)) v
y)) v (((y ^ (((x1 v (y v x2)) ^ (x3 v y)) ^ y)) v (u ^ (y v
(((x1 v (y v x2)) ^ (x3 v y)) ^ y)))) ^ (x v (((x1 ^ y) v (y ^
x2)) v y)))) ^ (((x ^ y) v (y ^ (x v y))) v z)) = y
This axiom, which we will refer to as LT-79, has length 79. To the best of our knowledge, this was the shortest known single axiom at the time the monograph was published.
In July 2001, we proved the following length 77 single axiom, LT-77.
(((xa ^ y) v (y ^ (xb v y))) ^ xc) v (((xd ^ (((xe ^ y) v (y ^ xf)) v
y)) v (((y ^ (((xg v (y v xh)) ^ (xi v y)) ^ y)) v (xj ^ (y v
(((y v x) ^ (xm v y)) ^ y)))) ^ (xn v (((xo ^ y) v (y ^
xp)) v y)))) ^ (((xq ^ y) v (y ^ (xr v y))) v xs)) = y
LT-77 can be derived as a simplification of LT-79 as follows.
(((xa ^ y) v (y ^ (xb v y))) ^ xc) v (((xd ^ (((xe ^ y) v (y ^ xf)) v
y)) v (((y ^ (((xg v (y v xh)) ^ (xi v y)) ^ y)) v (xj ^ (y v
(((xk v (y v xl)) ^ (xm v y)) ^ y)))) ^ (xn v (((xo ^ y) v (y ^
xp)) v y)))) ^ (((xq ^ y) v (y ^ (xr v y))) v xs)) = y
It is known that such a "variable generalized" version of a lattice identity
remains a lattice identity.
(xk v (y v xl))
by
(y v x),
where x is a new variable.
It is easy to see that LT-77 necessarily is an identity. To prove that it is a single axiom, it suffices to use it to derive a known basis. In our case, we derived the McKenzie basis (see page 137 of [2]):
x v (y ^ (x ^ z)) = x (L1) x ^ (y v (x v z)) = x (L2) ((y ^ x) v (x ^ z)) v x = x (L3) ((y v x) ^ (x v z)) ^ x = x (L4)
The proof, found with Otter ([1]), is here.
The reduction from length 79 to length 77 perhaps is less than exciting -- especially considering that we have since found and proved length 29 single axioms, but at the time of its discovery, LT-77 was the shortest known single axiom (as far as we know).
(((x ^ y) v (y ^ (x v y))) ^ z) v (((x ^ (((x1 ^ y) v (y ^ x2)) v
y)) v (((y ^ (((x1 v (y v x2)) ^ (x3 v y)) ^ y)) v (u ^ (y v
(((x1 v (y v x2)) ^ (x3 v y)) ^ y)))) ^ (x v (((x1 ^ y) v (y ^
x2)) v y)))) ^ (((x ^ y) v (y ^ (x v y))) v z)) = y,
which has 7 variables, and make a term replacement corresponding to
what we did previously, we get
(((x ^ y) v (y ^ (x v y))) ^ z) v (((x ^ (((x1 ^ y) v (y ^ x2)) v
y)) v (((y ^ (((x1 v (y v x2)) ^ (x3 v y)) ^ y)) v (u ^ (y v
(((y v xnew) ^ (x3 v y)) ^ y)))) ^ (x v (((x1 ^ y) v (y
^ x2)) v y)))) ^ (((x ^ y) v (y ^ (x v y))) v z)) = y,
where xnew is a new variable.
This new equation, LT-77a, is a same-length instance (by variable renaming)
of LT-77 and has 8 variables. The proof that LT-77a is a single axiom can be
found here.
We do not know if there can be a further reduction (by renaming) of the number of distinct variable names used. We also do not know if the other occurrence of the subterm (x1 v (y v x2)) can be replaced in a similar fashion.
[1] McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.
[2] McCune, W., and Padmanabahn, R., Automated deduction in equational logic and cubic curves, Lecture Notes in Computer Science 1095, Springer-Verlag, New York (1996).
[3] McCune, W., Padmanabahn, R., and Veroff, R., Yet another single law for lattices, Algebra Universalis, to appear. (postscript, pdf)