The weak/strong satisfiability problem for Quantum Logic over a fixed inner product space $V$ asks for whether a given Boolean expression $\varphi$ admits an assignment of subspaces of $V$ that makes $\varphi$ evaluate to a non-trivial subspace of/the entire space $V$. Its computational complexity is known to climb from trivial $d=0$ via the Boolean case $d=1$ and $d=2$ both NP-complete to every fixed higher dimension being polynomial-time equivalent to the Existential Theory of the Reals (Herrmann&Ziegler'11+2016).

We prove that strong satisfiability over SOME (i.e. additionally unbounded existentially quantified) dimension $d>0$ is undecidable.

More generally we consider, for a fixed class of algebraic structures of joint signature, the problem of whether a given conjunction of equations admits a satisfying assignment in some non-singleton member of the class; and, building on work by Bridson and Wilton (2015), show it to be undecidable for (i) the class of all subspace lattices of finite dimensional vector spaces over a fixed or arbitrary field of characteristic $0$, and for (ii) classes of (finite) rings with unit.

This joint work with Christian Herrmann (TU Darmstadt) and Yasuyuki Tsukamoto (Hakuryo High School) has recently appeared in the International Journal of Algebra and Computation.