Disentangling FDE-Based Paraconsistent Modal Logics

Abstract

The relationships between various modal logics based on Belnap and Dunn’s paraconsistent four-valued logic FDE are investigated. It is shown that the paraconsistent modal logic $\mathsf{BK}^\Box$, which lacks a primitive possibility operator $\Diamond$, is definitionally equivalent with the logic $\mathsf{BK}$, which has both $\Box$ and $\Diamond$ as primitive modalities. Next, a tableau calculus for the paraconsistent modal logic KN4 introduced by L. Goble is defined and used to show that KN4 is definitionally equivalent with $\mathsf{BK}^\Box$ without the absurdity constant. Moreover, a tableau calculus is defined for the modal bilattice logic MBL introduced and investigated by A. Jung, U. Rivieccio, and R. Jansana. MBL is a generalization of BK that in its Kripke semantics makes use of a four-valued accessibility relation. It is shown that MBL can be faithfully embedded into the bimodal logic $\mathsf{BK}^\Box \times \mathsf{BK}^\Box$ over the non-modal vocabulary of MBL. On the way from $\mathsf{BK}^\Box$ to MBL, the Fischer Servi-style modal logic $\mathsf{BK}^\mathsf{FS}$ is defined as the set of all modal formulas valid under a modified standard translation into first-order FDE, and $\mathsf{BK}^\mathsf{FS}$ is shown to be characterized by the class of all models for $\mathsf{BK}^{\Box }\times \mathsf{BK}^{\Box }$. Moreover, $\mathsf{BK}^\mathsf{FS}$ is axiomatized and this axiom system is proved to be strongly sound and complete with respect to the class of models for $\mathsf{BK}^{\Box }\times \mathsf{BK}^{\Box }$. Moreover, the notion of definitional equivalence is suitably weakened, so as to show that $\mathsf{BK}^\mathsf{FS}$ and $\mathsf{BK}^{\Box }\times \mathsf{BK}^{\Box }$ are weakly definitionally equivalent.