MiS Preprint Repository

We investigate the first-order theory of closed subspaces of complex Hilbert spaces in the signature $(\vee ,\perp ,0)$, where '$\perp$' is orthogonality. Our main result is that already its purely implicational fragment is undecidable: there is no algorithm to decide whether an implication between equations in the language of orthomodular lattices is valid in all complex Hilbert spaces. This is a simple corollary of a recent result of Slofstra in combinatorial group theory, and follows upon reinterpreting that result in terms of the hypergraph approach to contextuality.