Decidability of the Hilbert lattice and quantum logic What is known about the decidability of (first-order formulas in) the structure $(\mathcal{L}(H),\leq)$, where $\mathcal{L}(H)$ is the collection of all closed linear subspaces of a (separable) Hilbert space $H$, and $X\leq Y$ means $X\subseteq Y$? (Clearly meets and joins always exist and are first-order definable, so you can throw those in too.)
I can find some reference to the fact that this problem is open for infinite dimensional $H$, but known to be answered in the affirmative for finite dimensional $H$ (see: http://arxiv.org/pdf/math/0412144.pdf). I'm unfamiliar with the quantum logic literature, so references dealing with this question would be appreciated!
 A: A year after you posted the question, Fritz showed the common theory of all such lattices is undecidable:
https://arxiv.org/abs/1607.05870

In reponse to @MattF's query I'll post an example of how infinite dimension differs from finite. Namely, the lattice of closed subspaces is modular only in the finite-dimensional case. This is due to Birkhoff and von Neumann 1936  although they gave fewer details.
Let $e_1,e_2,\dots$ be a countable orthonormal basis for a separable subspace of your Hilbert space.
Let $A$, $B$ be respectively the closed subspace spanned by the vectors
$$a_n=e_{2n}+10^{-n}e_1+10^{-2n}e_{2n+1},\qquad b_n=e_{2n},$$
and let $C$ be spanned by $A\cup\{e_1\}$.
Then $B$ is incomparable with both $A$ and $C$ (under inclusion),
and $A$ is a proper subspace of $C$.

Let's prove that $A$ is a proper subspace of $C$.
  If not, $e_1$ should be expressible as a combination of vectors from $A$, i.e.,
  $$e_1=\sum k_na_n=\sum k_n e_{2n}+\sum k_n10^{-n}e_1+\sum k_n10^{-2n}e_{2n+1}=0$$
  since first and third terms must be 0, so that all the coefficients $k_n=0$.
  This gives the contradiction $e_1=0$.

The modular law requires that
$$A\subset C\implies A\vee (B\cap C)=(A\vee B)\cap C$$
but in this case we have
$$A=A\vee (B\cap C)\quad\text{and}\quad (A\vee B)\cap C=C,$$
so we have a counterexample.
On the other hand, in finite-dimensional Hilbert spaces the modular law does hold. 
