Labeled Sequent Calculus for Orthologic
Bulletin of the Section of Logic (2018)
- Volume: 47, Issue: 4
- ISSN: 0138-0680
Access Full Article
top
Abstract
topHow to cite
topTomoaki Kawano. "Labeled Sequent Calculus for Orthologic." Bulletin of the Section of Logic 47.4 (2018): null. <http://eudml.org/doc/295523>.
@article{TomoakiKawano2018,
abstract = {Orthologic (OL) is non-classical logic and has been studied as a part of quantumlogic. OL is based on an ortholattice and is also called minimal quantum logic. Sequent calculus is used as a tool for proof in logic and has been examinedfor several decades. Although there are many studies on sequent calculus forOL, these sequent calculi have some problems. In particular, they do not includeimplication connective and they are mostly incompatible with the cut-eliminationtheorem. In this paper, we introduce new labeled sequent calculus called LGOI, and show that this sequent calculus solve the above problems. It is alreadyknown that OL is decidable. We prove that decidability is preserved when theimplication connective is added to OL.},
author = {Tomoaki Kawano},
journal = {Bulletin of the Section of Logic},
keywords = {quantum logic; sequent calculus; cut-elimination theorem; decidability; Kripke model},
language = {eng},
number = {4},
pages = {null},
title = {Labeled Sequent Calculus for Orthologic},
url = {http://eudml.org/doc/295523},
volume = {47},
year = {2018},
}
TY - JOUR
AU - Tomoaki Kawano
TI - Labeled Sequent Calculus for Orthologic
JO - Bulletin of the Section of Logic
PY - 2018
VL - 47
IS - 4
SP - null
AB - Orthologic (OL) is non-classical logic and has been studied as a part of quantumlogic. OL is based on an ortholattice and is also called minimal quantum logic. Sequent calculus is used as a tool for proof in logic and has been examinedfor several decades. Although there are many studies on sequent calculus forOL, these sequent calculi have some problems. In particular, they do not includeimplication connective and they are mostly incompatible with the cut-eliminationtheorem. In this paper, we introduce new labeled sequent calculus called LGOI, and show that this sequent calculus solve the above problems. It is alreadyknown that OL is decidable. We prove that decidability is preserved when theimplication connective is added to OL.
LA - eng
KW - quantum logic; sequent calculus; cut-elimination theorem; decidability; Kripke model
UR - http://eudml.org/doc/295523
ER -
References
top- M. L. D. Chiara and R. Giuntini, Quantum Logics, Handbook of Philosophical Logic 2nd Edition 6 (2001), pp. 129–228.
- C. Faggian and G. Sambin, From Basic Logic to Quantum Logics with Cut-Elimination, International Journal of Theoretical Physics 37(1) (1998), pp. 31–37.
- G. M. Hardegree, Material Implication in Orthomodular (and Boolean) Lattices, Notre Dame Journal of Formal Logic 22(2) (1981), pp. 163–182.
- Z. Hou, A. Tiu and R. Gore, A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search, TABLEAUX 2013 (2013), pp. 172–187.
- S. Negri, Proof Analysis in Modal Logic, Journal of Philosophical Logic 34 (2005), pp. 507–544.
- S. Negri, Proof theory for modal logic, Philosophy Compass 6(8) (2011), pp. 523–538.
- H. Nishimura, Sequential Method in Quantum Logic, The Journal of Symbolic Logic 45(2) (1980), pp. 339–352.
- H. Nishimura, Proof Theory for Minimal Quantum Logic I, International Journal of Theoretical Physics 33(1) (1994), pp. 103–113.
- H. Nishimura, Proof Theory for Minimal Quantum Logic II, International Journal of Theoretical Physics 33(7) (1994), pp. 1427–1443.
NotesEmbed ?
topYou must be logged in to post comments.
To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.