Sequent Calculi for Orthologic with Strict Implication - Kawano, Tomoaki (Bulletin of the Section of Logic, 2021)
In this study, new sequent calculi for a minimal quantum logic (\(MQL\)) are discussed that involve an implication. The sequent calculus \(GO\) for \(MQL\) was established by Nishimura, and it is complete with respect to ortho-models (O-models). As \(GO\) does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \(GOI_1\) and \(GOI_2\) as the expansions of \(GO\). Both \(GOI_1\) and \(GOI_2\) 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.