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!