A double deduction system for quantum logic based on natural deduction (Q676184)

The projection operation \(\circ\) on an orthomodular lattice \(L\) is defined by \(b \circ a = b \land (\neg b \lor a)\). Elements \(a\) and \(b\) of \(L\) are said to be compatible if the mutually equivalent conditions \(a \circ b = b \circ a\), \(a \circ b = a \land b\) and \(a \circ b \leq b\) are fulfilled. The author presents a system of natural deduction, \textbf{QND-Prop}, for propositional quantum logic that includes rules based on the compatibility relation; it reduces to a classical system if all propositions are assumed to be mutually compatible. On the other hand, it seems that presence of this relation makes any cut elimination procedure for \textbf{QND-Prop} impossible. The system is shown to be both sound and complete w.r.t. the natural algebraic semantics -- the class of orthomodular lattices endowed with the compatibility relation. Some undesirable features of the logic proposed by \textit{P. Gibbins} [Logique Anal., Nouv. Sér. 28, 353-362 (1985; Zbl 0589.03039)] are eliminated in \textbf{QND-Prop}. The system is used to prove the following metatheorem: If \( \varphi[p_1,\ldots,p_n] \vdash \psi[p_1,\ldots,p_n] \) in classical logic, and if \(a_1, \ldots, a_n\) are mutually compatible propositions of quantum logic, then \( \varphi[a_1,\ldots,a_n] \vdash \psi[a_1,\ldots,a_n] \) in quantum logic. Semantically, compatible elements of an orthomodular lattice generate a Boolean subalgebra. The author claims that it is more difficult to state, and prove, this result in other systems of quantum logic.