A 4-basis for orthomodular lattices (OML) in terms of join (v), meet (^), and complement (c).

x v (y v z) = y v (x v z). % AJ x v (x ^ y) = x. % B1 x ^ y = c(c(x) v c(y)). % DM x v (c(x) ^ (x v y)) = x v y. % OMIf we add the orthomodular law OM to the ortholattice 5-basis { AJ, B1, DM, CC, ONE }, then CC and ONE become dependent. Here are Otter proofs.

otter < OML1.in > OML1.outHere are Mace2 jobs showing that the OML 4-basis is independent.

mace2 -N6 -p < OMLa.in > OMLa.out mace2 -N6 -p < OMLb.in > OMLb.out mace2 -N6 -p < OMLc.in > OMLc.out mace2 -N6 -p < OMLd.in > OMLd.out