Modal and Intuitionistic Variants of Extended Belnap-Dunn Logic with Classical Negation

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori's extended Belnap-Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding BD+ into BDi and the McKinsey-Tarski theorem for embedding BDi into BDm.

Automated summary

In this study, Gentzen-type sequent calculi BDm and BDi are introduced for modal extension and intuitionistic modification of extended Belnap-Dunn logic BD+ with classical negation. Theorems for embedding BDm and BDi into existing calculi for normal modal and intuitionistic logic are proven, leading to cut-elimination, decidability, and completeness theorems. Additionally, embedding theorems for BD+ into BDi and BDi into BDm are established, including Glivenko theorem and McKinsey-Tarski theorem.