Lattice Theory

Back to the Main Page

A 4-basis for lattice theory (LT) in terms of join (v) and meet (^).

    x v (y v z) = y v (x v z).  % AJ
    x ^ (y ^ z) = y ^ (x ^ z).  % AM
    x v (x ^ y) = x.            % B1
    x ^ (x v y) = x.            % B2
Note that this basis is self-dual (that is, the dual of each member is also a member).

A more standard basis for lattice theory is the 6-basis (also self-dual) consisting of B1, B2, and the commutativity and associativity of meet and join. Deriving commutativity of join (or of meet) from the 4-basis above shows that it is equivalent to the 6-basis. Here is an Otter proof of commutativity (idempotence is also proved).

    otter < LT1.in > LT1.out
The following two Mace2 jobs show independence of the LT 4-basis.
    mace2 -N6 -p < LTa.in > LTa.out
    mace2 -N6 -p < LTb.in > LTb.out