Natural deduction for quantum logic
type: Item
instance of: scholarly article
title: Natural deduction for quantum logic
zbMATH Open document ID: 1501.03005
author: Kenji Tokuo
published in: Logica Universalis
publication date: 2022-10-18T00:00:00Z
review text: 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)].
reviewed by: Hirokazu Nishimura
Mathematics Subject Classification ID: 03G12
Mathematics Subject Classification ID: 03B60
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 81P10
zbMATH DE Number: 7603237
zbMATH Keywords: quantum logic
zbMATH Keywords: natural deduction
zbMATH Keywords: \(\lambda\)-calculus
zbMATH Keywords: curry-howard isomorphism
zbMATH Keywords: normalization
MaRDI profile type: Publication
full work available at URL: s11787-022-00307-7
OpenAlex ID: W4289884257
cites work: An implication in orthologic
cites work: The axioms for implication in orthologic
cites work: Q3666849
cites work: Handbook of philosophical logic. Vol. 6
cites work: A double deduction system for quantum logic based on natural deduction
cites work: Nonmonotonicity and holicity in quantum logic
cites work: From basic logic to quantum logics with cut-elimination
cites work: Q3994895
cites work: The conditional in quantum logic
cites work: Q5427874
cites work: Implication connectives in orthomodular lattices
cites work: The deduction theorem for quantum logic—some negative results
cites work: Sequential method in quantum logic
cites work: Gentzen methods in quantum logic
cites work: Minimal quantum logic with merged implications
cites work: Q4240157
cites work: Normal proofs, cut free derivations and structural rules
cites work: Quantum implication
cites work: Basic logic: reflection, symmetry, visibility
cites work: A Lambda Calculus for Quantum Computation
cites work: A theory of computation based on quantum logic. I
DOI: 10.1007/S11787-022-00307-7
Recommended article: A double deduction system for quantum logic based on natural deduction
Recommended article: A new connective in natural deduction, and its application to quantum computing
Recommended article: LOGICS FROM QUANTUM COMPUTATION
Recommended article: Quantum logic in intuitionistic perspective
Recommended article: Natural deduction for non-classical logics
Recommended article: Q4342085
Recommended article: Q4224183
Recommended article: Axiomatization of quantum logics
Recommended article: Quantum logic and the classical propositional calculus
description: scientific article; zbMATH DE number 7603237