Ortholattice Independence Proofs

Many of the independence proofs are trivial, and it might seem like overkill to use Mace to find models showing independence.

The following rules could have been used instead of many of Mace's independence proofs.

• If the variety obeys any 3-variable associativity laws, then every basis must contain a law with at least three variables. Otherwise there can be nonassociative models.
• If the variety obeys any absorption laws, that is, laws of the form alpha=x, where alpha contains a variable different from x, then every basis must contain an absorption law.
• A basis cannot have the following property. In each equation, the leftmost variable of the left-hand side is the same as the leftmost variable of the right-hand side. Otherwise a left-hand projection model (xy=x) satisfies the basis. The same rule holds for the rightmost variables.