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. % B2Note 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.outThe 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