Decision problem for orthomodular lattices (Q1272084)

The author partially solves the problem of H. P. Sankappanavar and S. Burris whether the theory of orthomodular lattices is recursively inseparable and which varieties of orthomodular lattices are finitely decidable. Results: -- The variety of orthomodular lattices has a finitely inseparable first order theory. -- The variety of modular ortholattices is finitely decidable. -- The variety generated by the unique \(2n+2\) element modular ortholattice with \(2n\) atoms is finitely decidable. -- The variety generated by horizontal sums of Boolean algebras is finitely decidable.