Natural deduction for quantum logic (Q2084572)

A natural deduction for quantum logic was proposed in [\textit{Y. Delmas-Rigoutsos}, J. Philos. Log. 26, No. 1, 57--67 (1997; Zbl 0868.03029)]. Different from this, this paper proposes a natural deduction system corresponding to the reviewer's quantum sequent calculus \(\boldsymbol{GOM}\) [ J. Symb. Log. 45, 339--352 (1980; Zbl 0437.03034)]. While the reviewer's sequential system adopts conjunction (\(\wedge\)) and negation (\(\lnot\)) as basic operations, this paper adopts the Sasaki hook [\textit{U. Sasaki}, J. Sci. Hiroshima Univ., Ser. A 17, 293--302 (1954; Zbl 0055.25902)] as a kind of quasi-implication as well. Since the Sasaki hook fails to satisfy the deduction theorem, special care is required in dealing with assumptions. Once a natural deduction system for quantum logic is obtained, the corresponding quantum \(\lambda\)-calculus is introduced via the Curry-Howard correspondence. The proofs of the natural deduction system can be reversibly translated into the terms of the \(\lambda\)-calculus. The strong normalization property for the quantum \(\lambda\)-calculus is demonstrated. The proof of the strong normalization property follows [\textit{J.-Y. Girard} et al., Proofs and types. Cambridge etc.: Univ. Press (1989; Zbl 0671.68002)]. Some \(\lambda\)-calculi based on intuitionistic linear logic were studied under the name of quantum \(\lambda \)-calculus [\textit{P. Selinger} and \textit{B. Valiron}, in: Semantic techniques in quantum computation. Cambridge: Cambridge University Press. 135--172 (2010; Zbl 1344.68052); \textit{A. van Tonder}, SIAM J. Comput. 33, No. 5, 1109--1135 (2004; Zbl 1057.81016)].