Natural deduction for quantum logic
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)].
- A double deduction system for quantum logic based on natural deduction
- A new connective in natural deduction, and its application to quantum computing
- A new connective in natural deduction, and its application to quantum computing
- LOGICS FROM QUANTUM COMPUTATION
- Quantum logic in intuitionistic perspective
- Natural deduction for non-classical logics
- scientific article; zbMATH DE number 1028822
- scientific article; zbMATH DE number 1236960
- Axiomatization of quantum logics
- Quantum logic and the classical propositional calculus
- A double deduction system for quantum logic based on natural deduction
- A Lambda Calculus for Quantum Computation
- A theory of computation based on quantum logic. I
- An implication in orthologic
- Basic logic: reflection, symmetry, visibility
- From basic logic to quantum logics with cut-elimination
- Gentzen methods in quantum logic
- Handbook of philosophical logic. Vol. 6
- scientific article; zbMATH DE number 3819714 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1283787 (Why is no real title available?)
- Implication connectives in orthomodular lattices
- Minimal quantum logic with merged implications
- Nonmonotonicity and holicity in quantum logic
- Normal proofs, cut free derivations and structural rules
- Quantum implication
- Sequential method in quantum logic
- The axioms for implication in orthologic
- The conditional in quantum logic
- The deduction theorem for quantum logic—some negative results
- The source of the orthomodular law
- Strong normalization theorems for quantized -calculi
- On multiplicative linear logic, modality and quantum circuits
- Extending paraconsistent quantum logic: a single-antecedent/succedent system approach
- Natural Quantum Operational Semantics with Predicates
- Modal deduction systems for quantum state transformations
- A new connective in natural deduction, and its application to quantum computing
- A natural deduction system for orthomodular logic
This page was built for publication: Natural deduction for quantum logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2084572)
