Yet Another Single Law for Lattices

TEMPORARY: for the authors and the journal.
The final version for publication in Algebra Universalis:

William McCune, R. Padmanabhan, Robert Veroff

April 24, 2002

This page is associated with a paper (submitted for publication) of the same name.

A preprint (the submitted version) is available: DVI, PS, PDF.

Lattice Theory Bases

The two new single axioms are (length 29, 8 variables)

(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (w v ((v6 v x) ^ (x v v7))) = x.  % A1
(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x.  % A2

The McKenzie 4-basis is

x v (y ^ (x ^ z)) = x.
x ^ (y v (x v z)) = x.
((y ^ x) v (x ^ z)) v x = x.
((y v x) ^ (x v z)) ^ x = x.

Proofs

The short proof in the paper: A1 -> McKenzie-4-basis.
This uses the hints list to lead Otter to a specific short proof.
(The steps in proof in the paper were renumbered for better presentation.)

An "automatic" proof of A1 -> McKenzie-4-basis.

An "automatic" proof of A2 -> McKenzie-4-basis.

Previously Known Axioms

The length-79 axiom (7 variables) from [McCune-Padmanabhan:1996]:

(((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.

The length-77 axiom (8 variables) from [Veroff:2001]:

(((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.