Labeled Sequent Calculus for Orthologic
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...