Geodesic
Labeled Sequent Calculus for Orthologic
Bulletin of the Section of Logic, Tome 47 (2018) no. 4.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: quantum logic, sequent calculus, cut-elimination theorem, decidability, Kripke model 
@article{BSL_2018_47_4_a0,
     author = {Kawano, Tomoaki},
     title = {Labeled {Sequent} {Calculus} for {Orthologic}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {47},
     number = {4},
     year = {2018},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2018_47_4_a0/}
}
TY  - JOUR
AU  - Kawano, Tomoaki
TI  - Labeled Sequent Calculus for Orthologic
JO  - Bulletin of the Section of Logic
PY  - 2018
VL  - 47
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2018_47_4_a0/
LA  - en
ID  - BSL_2018_47_4_a0
ER  - 
%0 Journal Article
%A Kawano, Tomoaki
%T Labeled Sequent Calculus for Orthologic
%J Bulletin of the Section of Logic
%D 2018
%V 47
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2018_47_4_a0/
%G en
%F BSL_2018_47_4_a0
Kawano, Tomoaki. Labeled Sequent Calculus for Orthologic. Bulletin of the Section of Logic, Tome 47 (2018) no. 4. http://geodesic.mathdoc.fr/item/BSL_2018_47_4_a0/