Back to the Main Page

A 5-basis for ortholattices (OL) 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
If we start with the lattice theory 4-basis { AJ, AM, B1, B2 } and restrict that to the ortholattices by adding { DM, CC, ONE }, then AM and B2 become dependent. Here are Otter proofs.
    otter < OL1.in > OL1.out
    otter < OL2.in > OL2.out
Here are Mace2 jobs showing that the OL 5-basis given above is independent.
    mace2 -N6 -p < OLa.in > OLa.out
    mace2 -N6 -p < OLb.in > OLb.out
    mace2 -N6 -p < OLc.in > OLc.out
    mace2 -N6 -p < OLd.in > OLd.out
    mace2 -N6 -p < OLe.in > OLe.out