Orthomodular Lattices

The main result of the article is the solution to the problem of short axiomatizations of orthomodular ortholattices. Based on EQP/Otter results [10], we gave a set of three equations which is equivalent to the classical, much longer equational basis of such a class. Also the basic example of the lattice which is not orthomodular, i.e. benzene (or B⁶) is defined in two settings - as a relational structure (poset) and as a lattice.

As a preliminary work, we present the proofs of the dependence of other axiomatizations of ortholattices. The formalization of the properties of orthomodular lattices follows [4].