Modular Ortholattices

Back to the Main Page

A 6-basis for modular ortholattices (MOL) 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
    c(c(x)) = x.                % CC
    x v c(x) = y v c(y).        % ONE
    x v (y ^ (x v z)) = x v (z ^ (x v y)).  % MOD
This basis is simply our ortholattice 5-basis plus the modularity law MOD. The following Otter proof shows that the orthomodular law OM holds in MOL.
    otter < > MOL1.out
Here are Mace2 jobs showing that the MOL 6-basis is independent.
    mace2 -N6 -p < > MOLa.out
    mace2 -N6 -p < > MOLb.out
    mace2 -N6 -p < > MOLc.out
    mace2 -N6 -p < > MOLd.out
    mace2 -N6 -p < > MOLe.out
    mace2 -N6 -p < > MOLf.out
A more common modularity law is
    x v (y ^ (x v z)) = (x v y) ^ (x v z).   % MOD2
Here are Otter proofs that MOD and MOD2 are equivalent in lattice theory.
    otter <  > ML1.out
    otter <  > ML2.out