Abstract

In this study, new sequent calculi for a minimal quantum logic ) are discussed that involve an implication. The sequent calculus \ for \ was established by Nishimura, and it is complete with respect to ortho-models. As \ does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \ and \ as the expansions of \. Both \ and \ are complete with respect to the O-models. In this study, the completeness and decidability theorems for these new systems are proven. Furthermore, some details pertaining to new rules and the strict implication are discussed.