Nested-sequent Calculus for Modal Logic MB

TL;DR

This paper develops a nested-sequent calculus for the modal logic MB, addressing its completeness and decidability, and introduces an extended logic MB+ with additional modal symbols.

Contribution

It provides the first complete nested-sequent calculus for MB and explores an extended version MB+ with new modal operators.

Findings

Established completeness theorem for MB

Proved decidability of MB validity problem

Introduced and analyzed MB+ with additional modal symbols

Abstract

Quantum logic (QL) is a non-classical logic for analyzing the propositions of quantum physics. Modal logic MB, which is a logic that handles the value of the inner product that appears in quantum mechanics, was constructed with the development of QL. Although the basic properties of this logic have already been analyzed in a previous study, some essential parts still need to be completed. They are concerned with the completeness theorem and the decidability of the validity problem of this logic. This study solves those problems by constructing a nested-sequent calculus for MB. In addition, new logic MB+ with the addition of new modal symbols is discussed.