Modular Ortholattices

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.in > MOL1.out

Here are Mace2 jobs showing that the MOL 6-basis is independent.

    mace2 -N6 -p < MOLa.in > MOLa.out
    mace2 -N6 -p < MOLb.in > MOLb.out
    mace2 -N6 -p < MOLc.in > MOLc.out
    mace2 -N6 -p < MOLd.in > MOLd.out
    mace2 -N6 -p < MOLe.in > MOLe.out
    mace2 -N6 -p < MOLf.in > 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.in  > ML1.out
    otter < ML2.in  > ML2.out