A non-orthomodular orthocomplemented lattice identity? Assume you have an orthocomplemented (but possibly not orthomodular) lattice $L$.  For $q,r\in L$ say "$q$ and $r$ are in position $p'$" to mean that $q\wedge r^\perp=0$ and $r\wedge q^\perp=0$.  Is it true, for arbitrary $q,r\in L$, that $q'=q\wedge(q\wedge r^\perp)^\perp$ and $r'=r\wedge(r\wedge q^\perp)^\perp$ are in position $p'$?  If I'm not mistaken, this is true when $L$ is orthomodular, but also sometimes when it is not, for example when $L=O_6$, the simplest non-orthomodular orthocomplemented lattice.
Actually, just in general, does anyone know any good sources discussing non-orthomodular orthocomplemented lattices?
 A: You are interested in a ortholattice identity in two variables. Now, the word problem for free ortholattices and free orthomodular lattices is solvable; hence you can apply these algorithms to obtain an answer to your question (is a given identity valid in all ortholattices? all orthomodular lattices?).
For free ortholattices, see a paper by G. Bruns, canad. j. math.CJM-1976-095-6 (a Google scholar search also finds more modern papers, such as one by W. McCune - Information Processing Letters, 1998; one by A. Meinander - Mathematical Structures in Computer Science, 2010; and so on). You can also
try to find counterexamples using the examples of ortholattices that I have
just posted in another answer.
For free orthomodular lattices, you can check the references in G. Kalmabach classical book (in particoular, the free two-generated orthomodular lattice is finite, direct product of a Boolean component and a projective line, which makes the checking of a identity inmediate), and her paper of 1986 in Bull. Astral. math. soc. Also, books and papers about the syntactic aspects of quantum logics have related results (often for proper subvarieties of the variety of all orthomodular lattices, but sometimes also in quite general varieties). Some of them in the initial stages consider also non-orthomodular ortholattices and show many conditions equivalent to orthomodularity and some conditions strictly weaker but non trivial (a nice example is a paper of S. Maeda, 1966)
You can find much more with Google scholar searches.
