We shall be concerned with the modal logic BK—which is based on the Belnap–Dunn four-valued matrix, and can be viewed as being obtained from the least normal modal logic K by adding ‘strong negation’. Though all four values ‘truth’, ‘falsity’, ‘neither’ and ‘both’ are employed in its Kripke semantics, only the first two are expressible as terms. We show that expanding the original language of BK to include constants for ‘neither’ or/and ‘both’ leads to quite unexpected results. To be more (...) precise, adding one of these constants has the effect of eliminating the respective value at the level of BK-extensions. In particular, if one adds both of these, then the corresponding lattice of extensions turns out to be isomorphic to that of ordinary normal modal logics. (shrink)

We determine the modal logic of fixed-point models of truth and their axiomatizations by Solomon Feferman via Solovay-style completeness results. Given a fixed-point model $\mathcal {M}$, or an axiomatization S thereof, we find a modal logic M such that a modal sentence $\varphi $ is a theorem of M if and only if the sentence $\varphi ^*$ obtained by translating the modal operator with the truth predicate is true in $\mathcal {M}$ or a theorem of S under all such translations. (...) To this end, we introduce a novel version of possible worlds semantics featuring both classical and nonclassical worlds and establish the completeness of a family of noncongruent modal logics whose internal logic is nonclassical with respect to this semantics. (shrink)

The language of Belnap–Dunn modal logic \ expands the language of Belnap–Dunn four-valued logic with the modal operator \. We introduce the polarity semantics for \ and its two expansions \ and \ with value operators. The local finitary consequence relation \ in the language \ with respect to the class of all frames is axiomatized by a sequent system \ where \. We prove by using translations between sequents and formulas that these languages under the polarity semantics have the (...) same expressive power on the level of frames with the language \ under the relational semantics for classical modal logic. (shrink)

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. (shrink)

We investigate some non-normal variants of well-studied paraconsistent and paracomplete modal logics that are based on N. Belnap’s and M. Dunn’s four-valued logic. Our basic non-normal modal logics are characterized by a weak extensionality rule, which reflects the four-valued nature of underlying logics. Aside from introducing our basic framework of bi-neighbourhood semantics, we develop a correspondence theory in order to prove completeness results with respect to our neighbourhood semantics for non-normal variants of \, \ and \.