Lattice Laws Forcing Distributivity Under Unique Complementation

This is Version 3 of the Web page.
R. Padmanabhan, William McCune, Robert Veroff

August 2005

Proposed final version for Houston J. Math., January 19, 2006

Drafts

This Web page is a companion to a paper (in preparation) of the same name, and it serves several purposes. It fills in some proofs and details omitted from the paper, it is a tutorial on the use of the automated deduction, it is written in a more elementary style, and it serves as research notes for the project.

The automated deduction systems Prover9 and Otter (which search for proofs) and Mace4 (which searches for finite models and counterexamples) is used. Note that for these programs, x,y,z,... are variables; A,B,C, ... are constants; and implications are written as disjunctions.

Uniquely Complemented Lattices and Boolean Algebra

This work is on uniquely complemented lattices. Here are axioms (written in the laguage of Prover9 clauses). 
  % Lattice Theory (LT)

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

  % Existence of Complements

  x v x' = 1.
  x ^ x' = 0.

  % Unique Complementation (UC)

  x v y != 1 | x ^ y != 0 | x' = y.
A very basic theorem is that a complemented lattice satisfying either of the distributivity laws is a Boolean algebra, and we use that theorem as the basis of this work.

It is also well known that a UC lattice satisfying modularity is a Boolean algebra. Prover9 can prove this by deriving distributivity: 

    prover9 -f uc-mod.in > uc-mod.out
In ordinary lattice theory, modularity is weaker than distributivity, and this work extends that notion by presenting even wearker properties that force UC lattices to be Boolean.

Another property that forces a UC lattice to be Boolean is "order reversibilty", that is, the implication x ≤ y → y' ≤ x'. Here is a Prover9 proof that derives distributivity from the order reverseibility property. 

    prover9 -f ord-rev.in > ord-rev.out
This property is usually easier to prove than distributivity or modularity, so we use it in the proofs below.

Also see a first-order proof for Frink's basis for Boolean algebra: 

    prover9 -f frink.in > frink.out

Non-Modular Huntington Varieties

Theorem 1 from the paper: 
    prover9 -f H69.in > H69.out
Mace4 shows that H69 does not satisfy modularity (by giving N_5 as a counterexample): 
    mace4 -c -N100 -f H69-nonmod.in > H69-nonmod.out
Theorem 3 from the paper: 
    prover9 -f H58.in > H58.out

Huntington Implications

Consider the three implications (written as disjunctions, i.e., clauses for the theorem prover). 
   x v y != x v z  |  x v y = x v (y ^ z)                    # label(SD_join).
   x v y != x v z  |  (x ^ y) v (x ^ z) = x ^ (y v z)        # label(CD_join).
   x v y != x v z  |  x ^ ((x ^ y) v z) = (x ^ y) v (x ^ z)  # label(CM_join).
and their duals SD_meet, CD_meet, CM_meet.

Theorem 2 in the paper says that these are Huntington properties. Here are Prover9 proofs. 

    prover9 -f SD-join.in > SD-join.out 
    prover9 -f CD-join.in > CD-join.out 
    prover9 -f CM-join.in > CM-join.out
Each of the identities in the following lists is shown to be a Huntington identity by proving one of those six properties.

SD-join proofs

  x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ (y v u)))))  # label(H50).
  x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ u)))        # label(H51).
  x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (x ^ y))))        # label(H76).
  x ^ (y v (z ^ (x v u))) = x ^ ((x ^ (y v (x ^ z))) v (z ^ u))  # label(H79).

SD-meet proofs

  x ^ (y v z) = x ^ (y v (x ^ (z v (x ^ (y v (x ^ z))))))        # label(H64).
  x ^ (y v z) = x ^ (y v (x ^ (z v (x ^ y))))                    # label(H68).
  x ^ (z v y) = (x ^ (y v (x ^ z))) v (x ^ (z v (x ^ y)))        # label(H69).
  x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (x ^ y))))        # label(H76).
  x ^ (y v (z ^ (x v u))) = x ^ ((x ^ (y v (x ^ z))) v (z ^ u))  # label(H79).

CD-join proofs

  (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y)))        # label(H82).

CD-meet (none)

CM-join proofs

  (x ^ y) v (x ^ z) = x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z))))  # label(H18).
  (x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v (y ^ (x v z)))))  # label(H80).
  (x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y)))        # label(H82).

CD-meet (none)

Other Huntington Identities

The members of this set do not satisfy any of the six Huntington implications shown in the preceding section. 
x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ u))))        # label(H1).
x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z))))  # label(H2).
x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y))))))  # label(H3).
x v (y ^ (x v z)) = x v (y ^ (z v (x ^ (z v y))))              # label(H55).
x ^ (y v z) = x ^ (y v ((x v y) ^ (z v (x ^ y))))              # label(H58).  % Theorem 3
Here are the corresponding Prover9 proofs. 
  prover9 -f H1.in > H1.out 
  prover9 -f H2.in > H2.out 
  prover9 -f H3.in > H3.out 
  prover9 -f H55.in > H55.out 
  prover9 -f H58.in > H58.out
None of these five Huntington identities satisfies any of the six Huntington implications. Mace4 easily shows this by finding the counterexamples given in the following table. Each counterexample is the smallest possible.

SD-join SD-meet CD-join CD-meet CM-join CM-meet
H1 SD-join-H1.out SD-meet-H1.out CD-join-H1.out CD-meet-H1.out CM-join-H1.out CM-meet-H1.out
H2 SD-join-H2.out SD-meet-H2.out CD-join-H2.out CD-meet-H2.out CM-join-H2.out CM-meet-H2.out
H3 SD-join-H3.out SD-meet-H3.out CD-join-H3.out CD-meet-H3.out CM-join-H3.out CM-meet-H3.out
H55 SD-join-H55.out SD-meet-H55.out CD-join-H55.out CD-meet-H55.out CM-join-H55.out CM-meet-H55.out
H58 SD-join-H58.out SD-meet-H58.out CD-join-H58.out CD-meet-H58.out CM-join-H58.out CM-meet-H58.out

The Lattices

Here are the 15 covers of N5 and also M3, N5, and NM08. (Here are all 18 in tabular form.)

Note: Lattice NM08 (number 18) has been removed from the paper.

The Huntington Identities w.r.t. the Lattices

The following table shows the lattices that satisfy each of the Huntington identities. (Lattice 16 is M3, 17 is N5, and 18 is NM08.) 
x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ u))))       # label(H1).   %  1  2              7       10 11    13 14 15    17
x ^ (y v (x ^ z)) = x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) # label(H2).   %  1        4     6  7  8  9 10 11 12 13 14 15 16 17 18
x ^ (y v (x ^ z)) = x ^ (y v (z ^ (y v (x ^ (z v (x ^ y)))))) # label(H3).   %  1        4     6  7  8  9 10 11 12 13 14 15 16 17 18
(x ^ y) v (x ^ z) = x ^ ((x ^ y) v ((x ^ z) v (y ^ (x v z)))) # label(H18).  %  1        4     6  7     9 10 11    13    15 16 17 18
x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ (y v u))))) # label(H50).  %  1              6  7     9 10 11    13 14 15    17
x ^ (y v (z ^ (x v u))) = x ^ (y v ((x ^ z) v (z ^ u)))       # label(H51).  %  1                 7       10 11    13 14 15    17
x v (y ^ (x v z)) = x v (y ^ (z v (x ^ (z v y))))             # label(H55).  %     2        5  6  7  8  9 10    12 13 14 15 16 17 18
x ^ (y v z) = x ^ (y v ((x v y) ^ (z v (x ^ y))))             # label(H58).  %     2        5  6  7  8  9 10    12 13 14 15 16 17 18
x ^ (y v z) = x ^ (y v (x ^ (z v (x ^ (y v (x ^ z))))))       # label(H64).  %     2           6  7  8  9 10 11 12 13 14 15    17
x ^ (y v z) = x ^ (y v (x ^ (z v (x ^ y))))                   # label(H68).  %     2           6  7  8  9 10    12 13 14 15    17
x ^ (z v y) = (x ^ (y v (x ^ z))) v (x ^ (z v (x ^ y)))       # label(H69).  %     2           6  7  8  9 10    12 13 14 15    17
x ^ (y v (z ^ (y v u))) = x ^ (y v (z ^ (u v (x ^ y))))       # label(H76).  %                 6  7  8  9 10       13 14 15    17
x ^ (y v (z ^ (x v u))) = x ^ ((x ^ (y v (x ^ z))) v (z ^ u)) # label(H79).  %                    7       10       13 14 15    17
(x ^ y) v (x ^ z) = x ^ ((x ^ y) v (z ^ (x v (y ^ (x v z))))) # label(H80).  %  1     3  4     6  7  8  9 10 11    13    15 16 17 18
(x ^ y) v (x ^ z) = x ^ ((y ^ (x v z)) v (z ^ (x v y)))       # label(H82).  %  1        4     6  7     9 10 11    13    15    17
According to the table, the only pairs of identites that might be equivalent (given LT) are H2-H3, H55-H58, and H68-H69. The following Mace4 jobs show that they are not. In these five jobs, H2-H3, for example, shows that H2 does not imply H3. 
    mace4 -N100 -f H2-H3.in > H2-H3.out 
    mace4 -N100 -f H3-H2.in > H3-H2.out 
    mace4 -N100 -f H55-H58.in > H55-H58.out 
    mace4 -N100 -f H58-H55.in > H58-H55.out 
    mace4 -N100 -f H68-H69.in > H68-H69.out
Next we consider all implications that might hold (according to the table) between pairs of identities. For example, H82 might imply H80, because H80 holds in a subset of the 18 models in which H82 holds.

Disproved by Mace4 (in LT)

Mace4 easily finds finite counterexamples to the following four cases. 
    mace4 -N100 -f H18-H3.in > H18-H3.out 
    mace4 -N100 -f H76-H69.in > H76-H69.out 
    mace4 -N100 -f H79-H69.in > H79-H69.out 
    mace4 -N100 -f H82-H3.in > H82-H3.out

Proved with Prover9 (given LT)

These theorems were first proved with Otter or Prover9 by using variety of techniques, in particular with proof sketches, that is, by using proofs from previous cases as hints to guide the searches in subsequent cases.

Once we had the collection of theorems, we started from scratch, to get the proofs in a uniform way with Prover9. The proofs range from easy (e.g., H51->H1) to quite challenging (H50->H2). We started by trying to prove each without any hints. Then we iterated, using the proofs from the successful searches as hints for the failures. (Because the time limit was increased at each iteration, it is not always clear that the hints played a positive role.)

Only the proofs are given here. To reconstruct the input file, use "the basic input file" for each group.

Proved without hints (1 hour limit). All use this basic input file. 

    H18 -> H2
    H18 -> H80
    H50 -> H3
    H51 -> H1
    H51 -> H2
    H51 -> H3
    H68 -> H55
    H68 -> H58
    H68 -> H64
    H69 -> H55
    H69 -> H58
    H69 -> H64
    H69 -> H68
    H76 -> H2
    H76 -> H3
    H76 -> H55
    H76 -> H58
    H76 -> H64
    H76 -> H68
    H79 -> H1
    H79 -> H2
    H79 -> H3
    H79 -> H51
    H79 -> H55
    H79 -> H58
    H79 -> H64
    H79 -> H68
    H82 -> H18
    H82 -> H80
    H82 -> H2
Proved with hints from the preceding proofs (1 hour limit). Here is this basic input file. 
    H51 -> H50
    H79 -> H50
Proved with hints from all of the preceding proofs (1 hour limit). Here is this basic input file. 
    H50 -> H2
This following one was proved later. 
  prover9 -f H79-H76.in > H79-H76.out