Natural Deduction for Quantum Logic

Logica Universalis 16 (3):469-497 (2022)
  Copy   BIBTEX

Abstract

This paper presents a natural deduction system for orthomodular quantum logic. The system is shown to be provably equivalent to Nishimura’s quantum sequent calculus. Through the Curry–Howard isomorphism, quantum $$\lambda $$ -calculus is also introduced for which strong normalization property is established.

Categories

Keywords

Reprint years

DOI

10.1007/s11787-022-00307-7

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,830

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Natural deduction systems for Nelson's paraconsistent logic and its neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
The Significance of the Curry-Howard Isomorphism.Richard Zach - 2018 - In Gabriele Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics: Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin, Boston: De Gruyter. pp. 313-326.
Cut Elimination and Normalization for Generalized Single and Multi-Conclusion Sequent and Natural Deduction Calculi.Richard Zach - 2021 - Review of Symbolic Logic 14 (3):645-686.
The Curry-Howard Correspondence.Husna Farooqui - unknown
A double deduction system for quantum logic based on natural deduction.Yannis Delmas-Rigoutsos - 1997 - Journal of Philosophical Logic 26 (1):57-67.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Hypothetical Logic of Proofs.Eduardo Bonelli & Gabriela Steren - 2014 - Logica Universalis 8 (1):103-140.
A Substructural Gentzen Calculus for Orthomodular Quantum Logic.Davide Fazio, Antonio Ledda, Francesco Paoli & Gavin St John - 2023 - Review of Symbolic Logic 16 (4):1177-1198.
A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Reduction Rules for Intuitionistic $${{\lambda}{\rho}}$$ λ ρ -calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.

Analytics

Added to PP
2022-08-06

Downloads
32 (#699,889)

6 months
8 (#560,939)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A Natural Deduction System for Orthomodular Logic.Andre Kornell - 2024 - Review of Symbolic Logic 17 (3):910-949.

Add more citations

References found in this work

Implication connectives in orthomodular lattices.L. Herman, E. L. Marsden & R. Piziak - 1975 - Notre Dame Journal of Formal Logic 16 (3):305-328.
The conditional in quantum logic.Gary M. Hardegree - 1974 - Synthese 29 (1-4):63 - 80.

View all 7 references / Add more references