Natural deduction for quantum logic (Q2084572)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Natural deduction for quantum logic
scientific article

    Statements

    Natural deduction for quantum logic (English)
    0 references
    0 references
    18 October 2022
    0 references
    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)].
    0 references
    quantum logic
    0 references
    natural deduction
    0 references
    \(\lambda\)-calculus
    0 references
    curry-howard isomorphism
    0 references
    normalization
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references