Posted on the Web March 19, 2002. Last updated on March 20, 2002 by Bob Veroff.

# Lattice Theory

This page (still under development) will summarize our work in proving theorems and identifying and verifying simple axiom systems for lattice theory.

This is joint work with Bill McCune and R. Padmanabhan.

### Single Axioms

McCune and Padmanabhan present (Theorem LT-12 on page 144 of ) 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.

• First, rename variables so that every variable occurrence -- except for occurrences of the primary variable y -- has a unique name.
```   (((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.

• LT-77 then is derived by replacing the subterm
```   (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 ):

```   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 (), 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).

##### Simplification of LT-77
Recall that LT-77 was derived from the variable generalized version of LT-79. More recently, we considered the question of reducing the number of distinct variable names used. If we go back to the original version of LT-79,
```   (((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.

### References

 McCune, W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois, 1994.

 McCune, W., and Padmanabahn, R., Automated deduction in equational logic and cubic curves, Lecture Notes in Computer Science 1095, Springer-Verlag, New York (1996).

 McCune, W., Padmanabahn, R., and Veroff, R., Yet another single law for lattices, Algebra Universalis, to appear. (postscript, pdf)