A Modal Axiomatization of BK

What happens if we drop the axiom (K) and the necessitation rule from the usual axiomatic presentation of modal logic T? This system was first introduced by Ivlev (1988, Bull. Sect. Log., 17, 114–121). We show that this logic is a syntactical variant of the well-known paraconsistent logic BK (also known as mbCciw), which belongs to a large family of Brazilian paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Our approach is semantical, as BK can be characterized by a 3-valued non-deterministic matrix (Nmatrix); we show that this Nmatrix can alternatively be axiomatized in a modal vocabulary by more convenient axioms. This result links this family of paraconsistent logics to another line of research aimed at characterizing modal logics without possible worlds, initiated by the works of Kearns (1981, J. Symb. Log., 46, 77–86) and Ivlev (1988, Bull. Sect. Log., 17, 114–121). We will see that the modal logics T and S4 ⁠, as well as their corresponding versions without the necessitation rule, can be characterized with the help of simple refinements of this single Nmatrix. All of this shows that this logic can serve as a base for both modal logics and LFIs.