Orthomodular Lattices

Back to the Main Page

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.  % OM
If 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.out
Here 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