# 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.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
```