Quantum logic is undecidable (Q2663337)

The main result of this paper is the following theorem. Theorem. For a complex Hilbert space \(\mathcal{H}\), let \(\mathcal{C}\left( \mathcal{H}\right) \) denote the lattice of closed linear subspaces of \(\mathcal{H}\), let \(0,1\in\mathcal{C}\left( \mathcal{H}\right) \) stand for the zero and full subspaces, and let \(P_{1},P_{2},...\) be free variables taking values in \(\mathcal{C}\left( \mathcal{H}\right) \). Then there is no algorithm to decide whether a sentence of the form \[ \forall P_{1}...\forall P_{n}\left( E_{1}\wedge...\wedge E_{k}\rightarrow 0=1\right) \] holds for every \(\mathcal{H}\), where each \(E_{i}\)\ is a formula of one of the following two: \begin{itemize} \item an equation of the form \[ P_{i_{1}}\vee...\vee P_{i_{k}}=1 \] \item an orthogonality relation \[ P_{i_{1}}\perp P_{i_{2}} \] between two free variables. \end{itemize} That is to say, quantum logic is already undecidable even on quasi-identities [\textit{A. I. Mal'tsev}, Алгебраические системы (Russian). Moskva: Izdat. ''Nauka'' (1970; Zbl 0223.08001)]. The key ingredient leading to the above theorem is an undecidability result of \textit{W. Slofstra} [J. Am. Math. Soc. 33, No. 1, 1--56 (2020; Zbl 1480.20083)] depending in turn on [\textit{R. Cleve} et al., J. Math. Phys. 58, No. 1, 012202, 7 p. (2017; Zbl 1355.81048); \textit{R. Cleve} and \textit{R. Mittal}, Lect. Notes Comput. Sci. 8572, 320--331 (2014; Zbl 1364.91015)]. The author remarks the connection of Slofstra's work [loc. cit.] to quantum logic through the hypergraph approach to contextuality [\textit{A. Acín} et al., Commun. Math. Phys. 334, No. 2, 533--628 (2015; Zbl 1312.81010)]. It was shown in [\textit{L. Lipshitz}, Trans. Am. Math. Soc. 193, 171--180 (1974; Zbl 0288.02026)] that the purely implicational fragment of the theory of all \(\mathcal{C}\left( \mathbb{C}^{n}\right) \) is undecidable. \textit{M. A. E. H. Sherif} [Algebra Univers. 37, No. 1, 70--76 (1997; Zbl 0902.06012)] has shown that any first-order theory between orthomodular lattices and finite orthomodular lattices is undecidable, while \textit{C. Herrmann} [J. Symb. Log. 75, No. 3, 1102--1110 (2010; Zbl 1205.06005)] has established that the equational theory of the orthomodular lattice of projections of a finite von Neumann algebra factor is decidable.