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). % ONEIf 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.outHere 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