Weak Belnapian modal logic

Abstract

1 Introduction

This paper introduces a new candidate for the smallest logic in a certain family of many-valued modal logics.¹ Let us start by introducing the family in question; for a broader exposition on many-valued modal logics, see, e.g. [19, 20] and references therein.

The logics in this family were identified in [27] as first-degree entailment |$ \mathsf{(FDE)} $|-based modal logics, owning to the fact that they all extend the system of |$\mathsf{FDE}$|⁠. While |$\mathsf{FDE}$| was originally introduced [15] as the first-degree (meaning not containing nested implications) fragment of relevant logic |$\mathsf{E}$|⁠, it became a prominent system in its own right due, in part, to the interpretation given to it by Belnap (see [6,7,15]). Under this interpretation, |$\mathsf{FDE}$| corresponds to reasoning with information aggregated from various sources, as, for instance, a database might. Of a particular proposition |$p$| a database might receive information that it is true (and not false), false (and not true), true and false or neither true nor false. Accordingly, |$\mathsf{FDE}$| can be seen as a four-valued system with truth values |$ \mathsf{t} $|⁠, |$\mathsf{f} $|⁠, |$ \mathsf{b} $| and |$ \mathsf{n} $|⁠. Modal logics over |$\mathsf{FDE}$| include Priest’s |$ {\mathsf{K}}_{\mathsf{fde}} $| [29], Goble’s |$ \mathsf{KN4} $| [21], Belnapian modal logics |$ \mathsf{BK} $| and |$ {\mathsf{BK}}^{\mathsf{FS}} $| [26,27] as well as modal bilattice logic (MBL) [30].

Here, we will be primarily interested in Belnapian modal logic |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠. The former is a modal logic over the system |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$|⁠, which is the result of adding the falsity constant |$\mathsf{f}$| and Peirce’s law to Nelson’s logic [1,24] now commonly known as |$\mathsf{N4}$|⁠. The latter is a modal expansion of the bilattice logic with constants, [3,4] which we denote here as |$ \mathsf{BL} $|⁠. |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and |$\mathsf{BL}$| have a lot more in common than simply extending |$\mathsf{FDE}$|⁠. For starters, |$\mathsf{BL}$| is a conservative extension of |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and so |$\mathsf{BL}$| and |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| have the same |$\{ \wedge ,\vee ,\rightarrow ,{\sim },\mathsf{f} \}$|-fragment. This is notable in the case of implication specifically, since the implication is motivated differently for two systems: for |$ \mathsf{N4}^{\mathsf{f}}_{p} $| it naturally comes from Nelson’s logic; while for |$ \mathsf{BL} $| it is motivated by considerations related to the symmetry conditions of Avron [5]. Next, both of them are not contrapositive: neither |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| nor |$\mathsf{BL}$| are closed under the following contraposition rule |$\varphi \mathbin{\vdash }\psi /{\sim }\psi \mathbin{\vdash }{\sim }\varphi $|⁠. This is in a stark contrast with |$\mathsf{FDE}$| itself, for which two common axiom systems exist: one (e.g. [2]) has contraposition rule as a primitive and another ([17]) has it as an admissible but not derivable rule. Accordingly, when expanding |$\mathsf{FDE}$| with new connectives, one could think of contraposition either as an essential feature or as a happy accident that can be abandoned with no harm when considering expansions. Clearly, here we will adopt the latter stance. As a result of not being contrapositive the usual replacement rule fails for both systems: a key feature of logics we are interested in. To summarize, what we are really interested are non-contrapositive |$\mathsf{FDE}$|-based modal logics that share implication with |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and |$\mathsf{BL}$|⁠; we will keep referring to such systems as ‘|$\mathsf{FDE}$|-based modal logics’ in the interest of space.

The reason we will focus on |$\mathsf{BK}$| and |$\mathsf{MBL}$| is that both systems have some claims to giving rise to a minimal semantic framework, i.e. playing the same role for our family of logics as |$\mathsf{K}$| does for classical ones. The authors of [26] allude to it by calling |$\mathsf{BK}$| ‘the Belnapian version of the least normal modal logic |$\mathsf{K}$|’, while of |$\mathsf{MBL}$| its authors say [30] (the emphasis is original, the reference is adjusted):

We axiomatize the minimum modal logic over this lattice in the sense of [9], i.e. the logic determined by the class of all four-valued Kripke frames.

In fact, relational semantics of two systems are quite similar: both use four-valued valuations to evaluate propositional variables and one accessibility relation to interpret the necessity operator. The chief difference between the two is that frames for |$\mathsf{BK}$| include one two-valued accessibility relation while frames for |$\mathsf{MBL}$| include one four-valued one.

Yet looking at the syntax, it is clear that two systems are incomparable: each admits modal principles that the other does not. The question is then whether there is a unified semantic framework for |$\mathsf{FDE}$|-based modal logics at all. This question led to some attempts to bridge the gap between |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠. The one in [27] was done via an intermediate Belnapian modal logic |$ {\mathsf{BK}}^{\mathsf{FS}} $| that is closely related to Fischer Servi’s logic [18]. With regards to this the key result of [27] was that |$ \mathsf{MBL} $| can be embedded into the expansion of |$ {\mathsf{BK}}^{\mathsf{FS}} $| with bilattice operators. In [13] a kind of modular approach to |$\mathsf{FDE}$|-based modal logics was developed which allowed to express |$\mathsf{BK}$| and |$\mathsf{MBL}$| in a uniform way. Yet another one was hinted at in [14], where neighbourhood semantics for four-valued modal logics was investigated.

In this paper, we will introduce a new semantic framework that does not only generalize that of |$\mathsf{BK}$| and |$\mathsf{MBL}$| but also has its own intuitive reading. The corresponding logic we will call the weak Belnapian modal logic  |$\mathsf{WBK}$| and the family of logics it gives rise to—weakly normal modal logics. In fact, |$\mathsf{WBK}$| will come in two variants: |$\mathsf{WBK}^{n}$| over the language of |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and |$\mathsf{WBK}^{b}$|—its conservative extension with bilattice operators. This is done to make sure that we do not rely on bilattice operators in developing our framework on the one hand, and are able to actually show that it generalizes |$\mathsf{MBL}$| on the other. As it happens, |$\mathsf{WBK}$| also has a very neat axiomatisation.

This paper is organized as follows: Section 2 is for preliminaries. In Subsection 2.1, we outline the four-valued matrix |$ \mathcal{FOUR} $| and logics associated with it including |$ \mathsf{FDE} $|⁠, |$ {\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}} $| and |$ \mathsf{BL} $|⁠. In Subsection 2.2, some differences between the languages of |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and |$\mathsf{BL}$| are laid out. Then, modal logics |$\mathsf{BK}$| and |$\mathsf{MBL}$| are introduced in Subsection 2.3. In Section 3, we introduce weak Belnapian modal logic |$\mathsf{WBK}$| in its two variants: |$\mathsf{WBK}^{n}$| and |$\mathsf{WBK}^{b}$| in the languages of |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠, respectively. We provide their syntax and semantics and obtain the corresponding completeness results. Section 4 is dedicated to correspondence theory over |$\mathsf{WBK}$|⁠. There we will show, in particular, how the semantics of |$\mathsf{MBL}$| and |$\mathsf{BK}$| can be recovered by considering extensions of |$\mathsf{WBK}^{b}$| and |$\mathsf{WBK}^{n}$|⁠, respectively. Last but not least in Section 5, we explore expressive power of |$ \mathsf{WBK}^{b} $|—our weak Belnapian modal logic over the language |$\mathsf{BL}$|⁠. We will see that over this language a dual possibility operator can be expressed but also that |$ \mathsf{BK} $| and |$ \mathsf{MBL} $| can be shown to be definable fragments of |$\mathsf{WBK}^{b}$|⁠.

2 Preliminaries

Let us begin with a few definitions. A language  |$ {\mathcal{L}} $| is a finite set of connectives with their respective arities. Formulas of |$ {\mathcal{L}} $| are constructed as usual from a fixed countable set of propositional variables |$ \mathsf{Prop} $| using connectives in |$ {\mathcal{L}} $|⁠; the set of all formulas of |$ {\mathcal{L}} $| is denoted |$ \mathsf{Form}\,{\mathcal{L}} $|⁠. A substitution in |${\mathcal{L}}$| is any function |$ s:\mathsf{Form}\,{\mathcal{L}}\rightarrow \mathsf{Form}\,{\mathcal{L}} $| that commutes with all connectives in |$ {\mathcal{L}} $| (and maps all logical constants of |$ {\mathcal{L}} $| to themselves).

2.1 |$\mathsf{FDE}$| and its expansions

Let us formally introduce the matrix |$ \mathcal{FOUR} $| that characterizes |$\mathsf{FDE}$|⁠. Four elements of this matrix (as well as logical constants corresponding to them, should we need them) will be denoted |$ \mathsf{t} $| (true), |$ \mathsf{f} $| (false), |$ \mathsf{b} $| (both) and |$ \mathsf{n} $| (neither). Put |$ FOUR=\{ \mathsf{t},\mathsf{f},\mathsf{n},\mathsf{b} \} $|⁠; throughout the text |$\alpha $| and |$\beta $| will range over the elements of |$FOUR$|⁠. It will be convenient to identify these elements with subsets of classical truth values |$ TWO=\{ 0,1 \} $|⁠. Then our four values can be arranged to obtain the following neat structure:

When read vertically, this structure forms a (bounded distributive) lattice with the least element |$ \mathsf{f} $| and the largest element |$ \mathsf{t} $|⁠. The corresponding ordering relation is called the truth order and is denoted by |$ \leq _{t} $|⁠; its lattice meet and join are denoted |$ \wedge $| and |$ \vee $|⁠, respectively. We also need (strong) negation  |$ {\sim } $| which maps |$ \mathsf{t} $| to |$ \mathsf{f} $| and vice versa, while leaving |$ \mathsf{n} $| and |$ \mathsf{b} $| in place. Observe that our representation allows us to characterize |$ \leq _{t} $| as follows:

Given our representation, there is a clear sense in which each (⁠|$n$|-ary) operation |$f$| on |$ FOUR $| is defined by a pair of conditions: let us call |$ 1\in f(\alpha _{1},\dotsc ,\alpha _{n}) $| the verification condition of |$ f $| and |$ 0\in f(\alpha _{1},\dotsc ,\alpha _{n}) $| the falsification condition of |$ f $|⁠. For instance, verification and falsification conditions for |${\sim } $| are

We will list all of the verification/falsification conditions of connectives introduced in this and the next subsections in Table 1 for ease of access.

By designating values |$ \mathcal{D}=\{ \mathsf{t},\mathsf{b} \} $| (i.e. |$ a\in \mathcal{D}\text{ iff}\ 1\in a $|⁠) we obtain a matrix

which characterizes |$ \mathsf{FDE} $| [7].

By extending |$ \mathcal{FOUR} $| with new operations, we can characterize logics |$ {\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and |$ \mathsf{BL} $|⁠, which form non-modal bases for |$ \mathsf{BK} $| and |$ \mathsf{MBL} $|⁠, respectively. The languages of |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}} $| and |$\mathsf{BL}$| are (⁠|$ n $| stands for Nelson and |$ b $| is for bilattice), respectively:

Here, |$\rightarrow $| denotes the shared (weak) implication connective of two logics. Connectives |$\otimes $| and |$\oplus $| come from recognizing that |$\mathcal{FOUR}$| forms a bilattice [3]. There is one more natural ordering relation on |$ \mathcal{FOUR} $| with |$ \mathsf{n} $| as the least element and |$ \mathsf{b} $| as the largest. Under our representation, this ordering relation is simply that of set-theoretic inclusion; in the literature, it is sometimes called the knowledge order (e.g. [3]) or the information order (see [31, Footnote 5]). Then |$\otimes $| and |$\oplus $| are, respectively, meet and join with respect to this order. Consult Table 1 on the behavior of these operators.

Accordingly, the following matrices characterize |$ \mathsf{N4}^{\mathsf{f}}_{p} $| and |$ \mathsf{BL} $|⁠, respectively:

For |$ \mathsf{BL,} $| this result is established in [3], while for |$ \mathsf{N4}^{\mathsf{f}}_{p} $| it follows from the completeness result in [27] which, in particular, implies that |$ \mathsf{BL} $| is a conservative extension of |$ \mathsf{N4}^{\mathsf{f}}_{p} $|⁠. Before we formally state this result let us give a few more definitions.

A Hilbert-style axiom system for |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| can be obtained [26] by adding the following to an axiom system for classical logic in the language |$\{ \wedge ,\vee ,\rightarrow ,\mathsf{f} \}$| (for an axiom system for |$\mathsf{BL}$| see [3]):

By a logic we will understand any set of formulas |$L$| in a language |${\mathcal{L}}$| such that (i) |${\mathcal{L}}^{n}\subseteq{\mathcal{L}}$|⁠, (ii) |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}\subseteq L$|⁠, (iii) |$L$| is closed under modus ponens  |$\varphi ,\varphi \rightarrow \psi /\psi $| and (iv) under uniform substitution  |$ \varphi /s(\varphi ) $| (where |$ s $| is an arbitrary substitution in |${\mathcal{L}}$|⁠). By an extension of a logic |$L,$| we understand any logic |$L^{\prime}$| in the same language such that |$L\subseteq L^{\prime}$|⁠. With every logic let us associate its (local) consequence relation [23]: put |$\varGamma \mathbin{\vdash _{L}}\varphi $| if |$\varphi $| belongs to the closure of |$\varGamma \cup L$| under modus ponens. Clearly, according to this definition |$L=\{ \varphi \mid \varnothing \mathbin{\vdash _{L}}\varphi \}$|⁠.

In practice, this simply means that, say, |$\varphi \in \mathsf{BL}$| iff for any replacement |$h$| of propositional variables with elements of |$FOUR$| we have |$1\in h(\varphi )$|⁠. We will make extensive use of this theorem in the remainder of the paper.

From our definition of logic, it follows that:

One of the interesting aspects of logics like |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| and |$\mathsf{BL}$| is that weak implication |$\rightarrow $| does not induce a logical congruence relation. Or, in other words, they do not satisfy the usual replacement property with respect to the (weak) equivalence connective |$\varphi \leftrightarrow \psi :=(\varphi \rightarrow \psi )\wedge (\psi \rightarrow \varphi )$|⁠. For instance, using the completeness result above on can easily verify that |$ \mathsf{t}\leftrightarrow (p\rightarrow p)\in{\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}} $|⁠, but |$ {\sim }\mathsf{t}\leftrightarrow{\sim }(p\rightarrow p)\notin{\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}} $|⁠. Not all is lost though as there are weaker versions of the replacement property. The most important one is induced by the strong implication and strong equivalence connectives:

Observe that strong implication internalizes the truth order relation in the following sense

It will be helpful to remember the following simple proposition:

We say that a logic |$L$| satisfies the weak-replacement property if it is closed under all instances of the following rule

where |$ \chi (\psi ) $| denotes the result of replacing some occurrence of |$ \varphi $| in |$ \chi (\varphi ) $| with |$ \psi $|⁠. Note that the rule above has a small redundancy: according to (SIm) it is equivalent to |$\varphi \Leftrightarrow \psi /\chi (\varphi )\leftrightarrow \chi (\psi )$|⁠; with this in mind, it is clear that intuitively weak replacement says that a formula |$\varphi $| can be replaced with |$\psi $| as long as both they and their negations are equivalent in the usual sense. It can be readily seen that (see, e.g. [26]):

2.2 Functionally complete language |${\mathcal{L}}^{b}$| and its negations

Next we discuss some differences between languages |${\mathcal{L}}^{n}$| and |${\mathcal{L}}^{b}$|⁠. See Table 1 for the verification and falsification conditions of all connectives introduced in this subsection.

An important difference between two languages is that |$ {\mathcal{L}}^{b} $| is functionally complete in the sense that any function on |$ FOUR $| can be represented as a formula of this language [4]; the same does not hold for |$ {\mathcal{L}}^{n} $|⁠. One way to articulate this difference is with a connective |$ C(\varphi ,\psi ) $| called the combinator in [28], which can be characterized by

Intuitively, the combinator allows one, given any two formulas |$ \varphi $| and |$ \psi $|⁠, to produce a formula |$ C(\varphi ,\psi ) $| which is verified under the same conditions as |$ \varphi $| and is falsified under the same conditions as |$ \psi $|⁠. In [28], the authors use the combinator to establish a connection between the usual notion of definitional equivalence and the one fit for logics with strong negation (that lack replacement property). The combinator can be defined in |${\mathcal{L}}^{b}$| as |$C(\varphi ,\psi ):=(\varphi \vee \mathsf{n})\wedge (\psi \vee \mathsf{b})$|⁠, but—as we will see a bit later—cannot be defined in |${\mathcal{L}}^{n}$|⁠.

Let us recall that we already have a primitive strong negation connective |${\sim }$|⁠. Another natural negation connective often introduced in the language |${\mathcal{L}}^{n}$| is classical negation  |$ \neg _{c}\varphi :=\varphi \rightarrow \mathsf{f} $|⁠. It is called classical due to its definition and the fact that the |$ \{ \wedge ,\vee ,\rightarrow ,\neg _{c} \} $|-fragment of |$ \mathsf{BL} $| (and of |$ \mathsf{N4}^{\mathsf{f}}_{p}$|⁠) coincides with classical logic.

An alternative negation |$ \neg _{b} $| called Boolean negation can be introduced in |${\mathcal{L}}^{b}$| and is characterized by |$ \neg _{b} \alpha =TWO\setminus \alpha $|⁠. It is clear why we call this negation Boolean: one can look at |$ \mathcal{FOUR} $| as a four-element Boolean algebra in which case |$ \neg _{b} $| would be its negation. Note that as with |$ \neg _{c} $| this negation is not exactly the negation of classical logic, since Boolean algebra can be seen as a matrix with just |$ \mathsf{t} $| as its designated element, whereas |$ \mathcal{FOUR} $| have |$ \mathsf{t} $| and |$ \mathsf{b} $| designated. Observe also that since verification conditions of |$ \neg _{c} $| and |$ \neg _{b} $| coincide, |$ \{ \wedge ,\vee ,\rightarrow ,\neg _{b} \} $|-fragment of |$ \mathsf{BL} $| also coincides with classical logic. Arguably, Boolean negation behaves more like classical negation than |$ \neg _{c} $| does albeit with respect to |$ \Rightarrow $| rather than |$ \rightarrow $|⁠. For instance, the following are theorems of |$ \mathsf{BL} $| (use Theorem 1):

while the results of replacing |$ \neg _{b} $| with |$ \neg _{c} $| in these formulas are not. Functional completeness of |$ {\mathcal{L}}^{b} $| implies that Boolean negation can be expressed via a formula in |$ \mathsf{BL} $| and, in fact, we can give its explicit definition as |$ \neg _{b}\varphi := C(\neg _{c}\varphi ,{\sim }\neg _{c}{\sim }\varphi ) $|⁠. In contrast, it is easy to see that |$ \neg _{b} $| is not definable over |$ {\mathcal{L}}^{n} $| (and hence neither is the combinator).

As an aside, one could also naturally define Boolean implication |$ \varphi \supset \psi :=\neg _{b}\varphi \vee \psi $|⁠. This seems noteworthy since one could develop a family of logics over the language |$ \{ \wedge ,\vee ,\supset ,{\sim } \} $| plus, perhaps, some additional constants in parallel to how it was done for |$ {\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}} $| and |$ \mathsf{BL} $|⁠.

Finally, in the works on the bilattice logic [3], one more negation connective is prominently featured: a conflation connective, which interacts with the information order as |${\sim }$| does with the truth order. Conflation can be defined using Boolean negation as either |$\neg _{b}{\sim }\varphi $| or |${\sim }\neg _{b}\varphi $|⁠. We summarize differences between four negation connectives mentioned above via their truth tables:

It is important to keep in mind that among those only |${\sim }$| and |$\neg _{c}$| are available to us when working with the smaller of two languages (i.e. |${\mathcal{L}}^{n}$|⁠).

The following proposition lists some equivalences which will be useful to us later.

We can now turn to introducing modal logics |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠.

2.3 Modal logics |$\mathsf{BK}$| and |$\mathsf{MBL}$|

Originally, |$ \mathsf{BK} $| was introduced in [26] as a system with both |$ \Box $| and |$ \Diamond $| in the language. Later, in [27], its |$ \Diamond $|-free fragment |$ \mathsf{BK}^\Box $| was introduced, which is the system we will refer to as |$ \mathsf{BK} $| throughout this paper. There is no harm in doing so since |$ \mathsf{BK} $| (as originally introduced) and |$ \mathsf{BK}^\Box $| are definitionally equivalent via |$ \Diamond \varphi :={\sim }\Box{\sim }\varphi $| [27]. Hence, the languages of |$\mathsf{BK}$| and |$\mathsf{MBL}$| are |$ {\mathcal{L}}^{n}_\Box ={\mathcal{L}}^{n}\cup \{ \Box \} $| and |$ {\mathcal{L}}^{b}_\Box ={\mathcal{L}}^{b}\cup \{ \Box \} $|⁠, respectively.

Let us start with the semantics and proceed to the axiom systems later. First, we need four-valued versions of some familiar semantic notions. Suppose |$W$| is a non-empty set. One can treat a regular modal accessibility relation as a function |$R:W^{2}\rightarrow TWO$|⁠, which outputs classical truth values. Then a natural four-valued generalization would be a function |${\mathbb{R}}:W^{2}\rightarrow FOUR$|⁠. Such a function we call a four-valued accessibility relation (on |$W$|⁠). Similarly, a valuation |$V$| can be taken to be a function which maps a pair |$\langle x,p\rangle $| where |$x\in W$| and |$p\in \mathsf{Prop}$| to a classical truth value, so that the usual |$x\in v(p)$| corresponds to |$V(x,p)=1$|⁠. Accordingly, let us call a function |${\mathbb{V}}:W\times \mathsf{Prop}\rightarrow FOUR$| a four-valued valuation on |$W$|. A four-valued valuation can be extended to accommodate connectives from |${\mathcal{L}}^{b}$| in a natural way: for |$n$|-ary |$f\in{\mathcal{L}}^{b}$| simply put (where on the right are operations as they are defined in Table 1):³

The semantics for |$\mathsf{BK}$| [26,27] (here written in a slightly different form) is quite natural in that |$\Box $| gets exactly the same verification condition as in classical modal logic and a falsification condition which is its natural dual. As a result semantics for |$\mathsf{BK}$| uses exactly one two-valued accessibility relation, so that a |$\mathsf{BK}$|-frame is |${\mathcal{W}}=\langle W,R\rangle $|⁠, where |$W\neq \varnothing $| and |$R$| is a two-valued relation on |$W$|⁠; a four-valued valuation over |${\mathcal{W}}$| is extended to connectives in |${\mathcal{L}}^{n}$| via (4Val) and to modal formulas according to the following:

The semantics for |$\mathsf{MBL}$| [30] is obtained by generalizing to the four-valued case the first-order definition of |$\Box $| to obtain (note that strong implication is used in the definition):

Then an |$\mathsf{MBL}$|-frame is a pair |${\mathcal{W}}=\langle W,{\mathbb{R}}\rangle $| of a non-empty set and a four-valued accessibility relation. A valuation |${\mathbb{V}}$| is extended to connectives in |${\mathcal{L}}^{b}$| according to (4Val) and unpacking the definition above we get:

Observe that the condition |$0\in{\mathbb{R}}(x,y) $| is only used for the verification condition, while |$1\in{\mathbb{R}}(x,y)$| is used both for the verification and for the falsification condition.

Let us put a few more semantic notions in place using |$\mathsf{BK}$| here as an example, all of the definitions are virtually the same for |$\mathsf{MBL}$|⁠. For a |$\mathsf{BK}$|-frame |${\mathcal{W}}$| put |${\mathcal{W}}\mathbin{\vDash }\varphi $| if |$1\in{\mathbb{V}}(x,\varphi )$| for any valuation |${\mathbb{V}}$| over |${\mathcal{W}}$| and denote |$\mathsf{L}({\mathcal{W}}):=\{ \varphi \mid{\mathcal{W}}\mathbin{\vDash }\varphi \}$|⁠. For a class |${\mathcal{K}}$| of |$\mathsf{BK}$|-frames put |$ \varGamma \mathbin{\vDash _{{\mathcal{K}}}}\varphi $| if for any |${\mathcal{W}}=\langle W,R\rangle \in{\mathcal{K}}$|⁠, any valuation |${\mathbb{V}}$| over |${\mathcal{W}}$| and any |$x\in W$| we have

Finally, we say that an extension |$L$| of |$\mathsf{BK}$| is (strongly) sound and complete with respect to the class |${\mathcal{K}}$| of |$\mathsf{BK}$|-frames if |$\mathbin{\vdash _{L}}$| coincides with |$\mathbin{\vDash _{{\mathcal{K}}}}$|⁠.

Moving on to the syntax we will provide axiom systems for |$\mathsf{BK}$| and |$\mathsf{MBL}$| that are slightly different from the ones featured in [27]⁴ and [30], respectively. We arrive to them via a combination of reasoning in [13,14] and (SIm). Let us first list all relevant rules and axioms:

Then

• a Hilbert-style axiom system for |$\mathsf{BK}$| can be obtained by adding |$(\mathsf{Mon}^{+})$|⁠, |$(\mathsf{Mon}^{-})$|⁠, |$(\Box \mathsf{and})$|⁠, |$(\Box \mathsf{true})$| and |$(\mathsf{bk})$| to an axiom system for |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| (see [27] and also [1,25]);

• a Hilbert-style axiom system for |$\mathsf{MBL}$| can be obtained by adding |$(\mathsf{wMon})$|⁠, |$(\Box \mathsf{and})$|⁠, |$(\Box \mathsf{true})$| and |$(\mathsf{mbl})$| to an axiom system of |$\mathsf{BL}$| [3].

Note that the additional modal rules are not used directly in derivations, as before with each logic we associate its local consequence relation which only uses modus ponens in derivations. We can state the corresponding completeness results [27,30]:

Let us discuss the syntactic differences between two systems a little bit more. According to (SIm) a combination of |$(\mathsf{Mon}^{+})$| and |$(\mathsf{Mon}^{-})$| implies |$(\mathsf{wMon})$| (⁠|$w$| stands for weak in |$(\mathsf{wMon})$| exactly for this reason). Then the differences between two systems boil down to the following: for |$\mathsf{BK}$| one strengthens |$(\mathsf{wMon})$| to |$(\mathsf{Mon}^{+})$| and |$(\mathsf{Mon}^{-}) $| and adds |$(\mathsf{bk})$|⁠; for |$\mathsf{MBL}$| one simply adds |$(\mathsf{mbl})$|⁠. One can already see how this would imply that two systems are incomparable: |$\mathsf{MBL}$| is not closed under |$(\mathsf{Mon}^{+})$| and |$(\mathsf{Mon}^{-})$|⁠, while |$(\mathsf{mbl})$| contains constant |$\mathsf{n}$| and so could not possibly be in |$\mathsf{BK}$|⁠. One more way to articulate the differences between |$\mathsf{BK}$| and |$\mathsf{MBL}$| is to consider related necessitation principles. It is clear that |$\mathsf{BK}$| is closed under the usual necessitation rule |$\varphi /\Box \varphi $|⁠. Meanwhile, |$\mathsf{MBL}$| is not: using the completeness result above it is easy to see that |$\mathsf{b}\in \mathsf{MBL}$| but |$\Box \mathsf{b}\notin \mathsf{MBL}$|⁠. This reveals a way in which weak monotonicity forces a stricter requirement on something being necessary. Since in our framework a proposition can be true and false, the closure over the usual necessitation rule does not rule out a situation in which a proposition |$\varphi $| is both logically false (in the sense that |${\sim }\varphi $| is a theorem) and necessary (in the sense that |$\Box \varphi $| is a theorem). To contrast, a counterpart of the necessitation rule for |$\mathsf{MBL}$| is the weak necessitation rule  |$\varphi \Leftrightarrow \mathsf{t}/\Box \varphi $|⁠.

Essentially, the corollary says that if |$\varphi $| is a theorem and |${\sim }\varphi $| is a counter-theorem of |$\mathsf{MBL}$|⁠, then |$\varphi $| is logically necessary, while for |$\mathsf{BK}$| the first requirement is enough.

3 Weak Belnapian modal logic

We are now ready to introduce the weak Belnapian modal logic |$\mathsf{WBK}$|⁠. As was discussed before it comes in two versions: |$\mathsf{WBK}^{n}$| in the language |${\mathcal{L}}^{n}_\Box $| and |$\mathsf{WBK}^{b}$| in the language |${\mathcal{L}}^{b}_\Box $|⁠.

The modal principles underlying |$\mathsf{WBK}$| are just shared axioms and rule of |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠:

Then an axiom system for |$\mathsf{WBK}^{n}$| (⁠|$\mathsf{WBK}^{b}$|⁠) is obtained from an axiom system for |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| (⁠|$\mathsf{BL}$|⁠) by adding |$(\mathsf{wMon})$|⁠, |$(\Box \mathsf{and})$| and |$(\Box \mathsf{true})$|⁠. Observe that this axiomatization is quite elegant in that it is a variant of axioms and rules for |$\mathsf{K}$| with strong implication in place of weak implication. One simply has to notice that |$\Box \varphi $| and |$\mathsf{t}\rightarrow \Box \mathsf{t}$| are classically equivalent formulas. Note also that |$(\Box \mathsf{true})$| is stronger than formula |$\Box \mathsf{t}$|⁠: it additionally implies that |${\sim }\Box \mathsf{t}$| is a counter-theorem of the logic.

For the purpose of this paper by a weakly normal modal logic let us call any logic that contains |$\mathsf{WBK}^{n}$| and is closed under |$(\mathsf{wMon})$|⁠. Clearly, |$\mathsf{BK}$| and |$\mathsf{MBL}$| qualify. Suppose |$L$| is a weakly normal modal logic, |$(\mathsf{ax})$| is a formula and |$(\mathsf{Rule})$| is a rule of inference, then the set of all weakly normal extensions of |$L$| is denoted |${\mathcal{E}} L$|⁠; |$ L \oplus (\mathsf{ax}) $| denotes the smallest |$L^{\prime}\in{\mathcal{E}} L,$| which contains |$(\mathsf{ax}) $|⁠; |$L\oplus (\mathsf{Rule})$| denotes the smallest |$L^{\prime}\in{\mathcal{E}} L$| which is closed under |$(\mathsf{Rule})$|⁠.

As before, the deduction property holds for any |$L\in{\mathcal{E}}\mathsf{WBK}$|⁠. Weak monotonicity rule also allows us to establish the weak replacement property.

Let us turn to the semantics. To better conceptualize this semantics, let us first reframe the usual verification condition for necessity in yet another way. Take

Then the condition on the right essentially says that |$V(y,\varphi )$| is at least as true as  |$R(x,y)$| for any |$y$|⁠. In our four-valued framework, the ‘at least as true’ relation can be expressed with |$\leq _{t}$|⁠. Then one four-valued generalization of this condition would be

This is the intuition behind our semantics.

Then a |$\mathsf{WBK}$|-frame is |${\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $|⁠, where |$W\neq \varnothing $| and |${\mathbb{R}}^{+}$|⁠, |${\mathbb{R}}^{-}$| are four-valued accessibility relations on |$W$|⁠. A valuation |${\mathbb{V}}$| over |${\mathcal{W}}$| is extended to formulas in the languages |${\mathcal{L}}^{n}$| and |${\mathcal{L}}^{b}$| according to (4Val) and to modal formulas via:

Unpacking these conditions, we get:

All of the semantic notions are defined exactly as in the previous section.

Let us make a couple of comments. Firstly, why do we have two different accessibility relations? Simply put because our modal axioms are not strong enough to force them to coincide; even though this makes for a less intuitive semantics it also makes for a more general one which is what we are aiming for. Secondly, there is a number of equivalent semantic clauses we could have given; these particular ones are motivated by (i) staying close to the semantics of |$ \mathsf{BK} $| and |$ \mathsf{MBL} $| and (ii) their intuitive reading.

Our first order of business is to prove the completeness result of |$\mathsf{WBK}$| with respect to |$\mathsf{WBK}$|-frames. We establish the result for |$\mathsf{WBK}^{b}$| since the proof is exactly the same in the case of |$\mathsf{WBK}^{n}$|⁠.

Now, let us fix |$ L \in{\mathcal{E}}\mathsf{WBK}^{b}$| for the remainder of the subsection. By a prime |$ L $|-theory we understand a set of formulas |$ \varGamma $| such that (i) |$ \varGamma $| is non-trivial: |$ \varGamma \neq \mathsf{Form}\,{\mathcal{L}}^{b}_\Box $|⁠; (ii) |$ \varGamma $| is closed under derivations: |$ \varGamma \mathbin{\vdash _{L}}\varphi $| implies |$ \varphi \in \varGamma $| and (iii) |$ \varGamma $| satisfies disjunction property: |$ \varphi \vee \psi \in \varGamma $| implies |$ \varphi \in \varGamma $| or |$ \psi \in \varGamma $|⁠. For sets of formulas |$\varGamma $| and |$\varDelta $| with |$\varDelta \neq \varnothing $| put

An important property of prime theories is the following, which follows from the fact that |$p\vee \neg _{c} p$| and |$ (p\wedge \neg _{c} p)\rightarrow q$| are theorems of |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$|⁠:

As usually, we get:

The canonical |$ L $|-frame is |$ {\mathcal{W}}_{L}=\langle W_{L},{\mathbb{R}}^{+}_{L},{\mathbb{R}}^{-}_{L}\rangle $|⁠, where |$ W_{L} $| is the set of all prime |$ L $|-theories and |$ {\mathbb{R}}^{+}_{L}, {\mathbb{R}}^{-}_{L} $| are defined as follows:

Observe that the condition in the first row is exactly that of the canonical accessibility relation for classical modal logics. The canonical |$ L $|-valuation  |$ {\mathbb{V}}_{L} $| over |$ {\mathcal{W}}_{L} $| is defined via

We say that a |$\mathsf{WBK}^{b}$|-frame |${\mathcal{W}}$| is an |$L$|-frame if |$L\subseteq \mathsf{L}({\mathcal{W}})$|⁠. We say that |$ L$| is canonical, if its canonical frame |${\mathcal{W}}_{L}$| is an |$L$|-frame.

4 Some extensions

In this section, we will consider some extensions that straightforwardly simplify the semantics before showing that our framework does indeed generalize those of |$\mathsf{MBL}$| and |$ \mathsf{BK}$|⁠. Simplifications will come in two forms: first, via replacing |$(\Box ^{+}{:}\mathsf{WBK})$| and |$(\Box ^{-}{:}\mathsf{WBK})$| with simpler conditions in the presence of some rules and then by expressing the case when |${\mathbb{R}}^{+}={\mathbb{R}}^{-}$|⁠. Here for the first time the differences between |$\mathsf{WBK}^{n}$| and |$\mathsf{WBK}^{b}$| will become important. As it turns out, things are a bit more awkward over the smaller of two languages. Let us point out that every non-modal connective |$f$| not definable in |${\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}}$| is also not definable in |$\mathsf{WBK}^{n}$|⁠. We can demonstrate this using Boolean negation as an example:

Let us start by strengthening the weak monotonicity rule, which will result in simpler verification and falsification conditions for the necessity operator. Note that by (SIm), the weak monotonicity rule is equivalent to the following pair of rules:

Then one can strengthen these rules by eliminating one of the premises. This gives us the following four rules, two of which we have already seen before:

For these rules, our strategy will differ from the usual correspondence theory [8]. Instead of finding frame-conditions corresponding to these rules, we will see how adding one of these rules allows one to directly modify the verification or falsification condition for our modal operator. Note that the usual strategy works well over the bigger language |${\mathcal{L}}^{b}$| but does not seem to be applicable over |${\mathcal{L}}^{n}$|⁠. In fact, over |${\mathcal{L}}^{b}$| every one of these rules is equivalent—in a sense that will be made clear shortly—to a formula and for these formulas one can find the corresponding frame-conditions as usual. There does not seem to be any real advantages to establishing these correspondences as compared to the results obtained here. Nevertheless, we will see one example of such a correspondence while expressing |$\mathsf{MBL}$| later in the section.

We introduce new verification and falsification conditions corresponding to these rules:

Fix |$\mathsf{Rule}\in \{ \mathsf{Mon},\mathsf{Con} \}$| and |$\delta \in \{ +,- \}$|⁠. Then a |$\mathsf{WBK}$|-frame respecting |$(\mathsf{Rule}^\delta ) $| is exactly the same as a |$\mathsf{WBK}$|-frame except when extending a valuation |${\mathbb{V}}$| over |${\mathcal{W}}$| we replace |$(\Box ^\delta :\mathsf{WBK})$| with |$(\Box ^\delta :\mathsf{Rule}^\delta )$|⁠. Straightforwardly adopting all of the notions from the previous section to the new semantics we get:

Next, we want to see how two accessibility relations can be reduced to one. Over |$\mathcal{FOUR}$| there are a lot of different ways of doing so: for instance, for any unary connective |$\theta $| one could try to demand that |${\mathbb{R}}^{-}=\ominus{\mathbb{R}}^{+}$| (or the other way around). Here, we will find formulas corresponding to properties |${\mathbb{R}}^{+}(x,y)\leq _{t}{\mathbb{R}}^{-}(x,y)$| and |${\mathbb{R}}^{-}(x,y)\leq _{t}{\mathbb{R}}^{+}(x,y)$|⁠, which seems to be the most natural choice given the framework.

Working over the functionally complete language |${\mathcal{L}}^{b}$| one can actually give somewhat more elegant formulas to express the equivalence between |${\mathbb{R}}^{+}$| and |${\mathbb{R}}^{-}$| using Boolean negation.

We say that a formula |$\varphi $| is canonical over |$\mathsf{WBK}$| if |$\varphi \in L$| implies |${\mathcal{W}}_{L}\mathbin{\vDash }\varphi $| for any |$L\in{\mathcal{E}}\mathsf{WBK}$|⁠. As usual, the addition of canonical formulas preserves the canonicity of a logic.

Clearly, for canonical extensions of |$ \mathsf{WBK} $| containing both formulas discussed in the previous lemma, we can provide equivalent semantics that involves only one accessibility relation |$ {\mathbb{R}} $| with the following verification/falsification conditions:

4.1 Expressing |$\mathsf{MBL}$|

We move on to consider how the semantics of |$ \mathsf{MBL} $| can be recovered from that of |$\mathsf{WBK}^{b}\oplus (\mathsf{mbl})$|⁠. Recall that

We will analyze four conjuncts of |$ (\mathsf{mbl}) $| separately. Put

First let us find out how formulas of the form |$ \mathsf{n}\Rightarrow \varphi $| behave. One can easily compute that

for any valuation |${\mathbb{V}}$| over a |$\mathsf{WBK}^{b}$|-frame |${\mathcal{M}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| and |$x\in W$|⁠. Using the completeness result we can extract from this a few useful equivalences.

From this, we can see that |$(\mathsf{mbl}_{4})$| is actually redundant:

Here one can see the differences between two approaches to proving completeness in the presence of |$(\mathsf{Mon}^{-})$| discussed in the previous subsection. The strategy adopted there amounted to observing that in the presence of this rule whether |${\sim }\Box \varphi $| belongs to some prime |$L$|-theory |$\varGamma $| does not depend on the condition |$1\in{\mathbb{R}}_{L}^{-}(\varGamma ,\varDelta )$| for any |$\varDelta $|⁠. Over |$\mathsf{WBK}^{b}$| one obtains a somewhat stronger result: that |$1\in{\mathbb{R}}_{L}^{-}(\varGamma ,\varDelta )$| simply never holds. This requires providing an explicit example of |$\varphi $| such that |${\sim }\Box \varphi \notin \varGamma $| and |$\varphi \notin \varDelta $|⁠, for which |$\varphi =\mathsf{n}$| qualifies. The language of |$\mathsf{WBK}^{n}$|⁠, on the other hand, does not seem to be strong enough to provide such a formula, which is why the usual method fails (or at least seems to fail). Still, as we have discussed above, two strategies are equally robust in the sense of being preserved for canonical extensions.

Let us proceed to consider formulas |$ (\mathsf{mbl}_{1}) $| and |$ (\mathsf{mbl}_{2}) $|⁠. We have the following verification conditions of two formulas involved, where |${\mathbb{V}}$| is a valuation over a |$\mathsf{WBK}^{b}$|-frame |${\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| and |$x\in W$| (see (3)):

Observe that from Propositions 11 and 12, it follows that |$(\mathsf{mbl}_{2})$| implies |$(\mathsf{mbl}_{3})$|⁠. The completeness result for |$\mathsf{WBK}^{b}\oplus (\mathsf{mbl})$| follows from the following lemma.

We can summarize the frame conditions corresponding to the axiom |$ (\mathsf{mbl}) $|⁠.

It follows that for any valuation |${\mathbb{V}}$| over a |$ \mathsf{WBK}^{b}$|-frame |${\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| such that |${\mathcal{W}}\mathbin{\vDash }(\mathsf{mbl})$| we have the following equivalent verification and falsification conditions for modal formulas:

These are clearly notational variants of |$(\Box ^{+}{:}\mathsf{MBL})$| and |$(\Box ^{-}{:}\mathsf{MBL})$|⁠, respectively, and since there is no more use for |${\mathbb{R}}^{-}$|⁠, we can drop it entirely to arrive to the semantics of |$\mathsf{MBL}$|⁠.

Observe that these results, perhaps, surprisingly imply that over |$ \mathsf{WBK}^{b} $| formula |$ (\mathsf{mbl}) $| has exactly the same strength as its two ‘positive’ conjuncts, that is as |$ (\mathsf{n}\Rightarrow \Box p)\leftrightarrow \Box (\mathsf{n}\Rightarrow p) $|⁠, which, in turn, means that the axiomatization of |$\mathsf{MBL}$| in [30] can be refined.

4.2 Expressing |$\mathsf{BK}$|

In this subsection, we will show how the semantics of |$\mathsf{BK}$| can be recovered from that of |$\mathsf{WBK}^{b}\oplus (Mon^{+})\oplus (\mathsf{bk})$|⁠. In particular, we will show that |$(\mathsf{bk})$| implies |$(Mon^{-})$|⁠. Recall that:

As in the previous subsection, we will start working with two conjuncts of this formula separately before encountering some hurdles:

Before we proceed, fix a valuation |${\mathbb{V}}$| over a |$\mathsf{WBK}^{n}$|-frame |$ {\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| and |$x\in W$|⁠. First, it is easy to see that for any |$\varphi $|⁠:

Using this, we can obtain the following equivalences ((6) is only used for the second one):

Surprisingly, the proof of canonicity for |$(\mathsf{bk}_{2})$| does not seem to go through and the problem feels similar to the one we encountered when dealing with monotonicity rules over the smaller language at the beginning of the section. To sidestep this problem, one can notice that the presence of |$(\mathsf{bk})$| implies that the corresponding logic is closed under |$(\mathsf{Mon}^{-})$|⁠. And, as it turns out, |$(\mathsf{bk})$| can be proved to be canonical over frames respecting |$(\mathsf{Mon}^{-})$|⁠. First, as an easy consequence of the previous proposition we get

That |$(\mathsf{bk})$| is canonical over |$\mathsf{WBK}^{n}\oplus (\mathsf{Mon}^{+})\oplus (\mathsf{Mon}^{-})$| follows directly from Lemma 6. All that remains is to confirm that the semantics of |$\mathsf{BK}$| can be recovered from that of |$\mathsf{WBK}^{n}\oplus (\mathsf{Mon}^{-})\oplus (\mathsf{bk})$|⁠. Take a |$\mathsf{WBK}^{n}$|-frame |${\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| respecting |$(\mathsf{Mon}^{+}) $| and |$(\mathsf{Mon}^{-})$| such that |${\mathcal{W}}\mathbin{\vDash }(\mathsf{bk})$|⁠. Then combining |$(\Box ^{+}{:}\mathsf{Mon}^{+})$| and |$(\Box ^{-}{:}\mathsf{Mon}^{-})$| with the results of the previous proposition gives us (where |${\mathbb{V}}$| is a valuation and |$x\in W$|⁠):

These are clearly notational variants of |$(\Box ^{+}{:}\mathsf{BK})$| and |$(\Box ^{-}{:}\mathsf{BK})$| obtained by defining a two-valued accessibility relation |$R$| via |$R(x,y)=1$| iff |$1\in{\mathbb{R}}^{+}(x,y)$|⁠.

5 Some variants and expressive power

In this section, we conclude the paper with a number of simple results concerning the expressive power of |$ \mathsf{WBK}^{b} $|—the version of our system over the functionally complete language. It is well known that over classical logic it is enough to consider only theories of necessity, since other common types of modal operators (possibility, unnecessity, impossibility) can be reduced to necessity via classical negation (but see [22] and references therein). This is often not the case for non-classical modal logics, for instance, [10] (see also [11,12]) contains two independent theories of intuitionistic modal logics corresponding to necessity and possibility, respectively. Both theories are meaningful, since intuitionistic negation is not strong enough to allow one to be defined through the other and vice versa. The question is then, should we define the theory of weak possibility on par with our theory of weak necessity? Turns out that in this regard |$ \mathsf{WBK}^{b} $| behaves more like classical logic and |$\mathsf{WBK}^{n}$|—more like intuitionistic.

Let us develop a weakly normal logic of the possibility operator while skipping most the proofs, as they are virtually the same as in Section 3. Denote by |$ \mathsf{WBK}^{n}_\Diamond $| the result of extending |$ {\mathsf{N4}}^{\mathsf{f}}_{\mathsf{p}} $| and by |$\mathsf{WBK}^{b}_\Diamond $| the result of extending |$\mathsf{BL}$| with the following

As before |$\mathsf{WBK}_\Diamond $| will denote either of two systems in situations which apply to both. Observe again that these axioms and rule are almost the same as the usual axiomatization for the possibility operator except with strong implication in place of weak implication.

In providing semantics for these axioms, we are guided by two considerations. First, that the verification condition of possibility should align with the usual satisfaction clause of classical modal logic. And second, that it should in some sense be dual to the semantics for necessity. With this in mind we arrive to the following:

This, in turn, can be put more succinctly as:⁸

Then we define a |$ \mathsf{WBK}_\Diamond $|-frame  |${\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| in exactly the same way as a |$ \mathsf{WBK} $|-frame and a valuation |${\mathbb{V}}$| over |${\mathcal{W}}$| is extended to the set of all formulas via (4Val) in non-modal cases and as above for the possibility operator. All of the other notions from Section 3 can be adopted straightforwardly.

The completeness result of |$ \mathsf{WBK}_\Diamond $| with respect to this semantics can be established exactly as in Section 3, expect we use the following definitions for the accessibility relations:

Then it turns out that this possibility operator can defined from the necessity operator as |$ \Diamond \varphi :=\neg _{b}\Box \neg _{b}\varphi $|⁠. Notably, as the presence of Boolean negation suggests, this only works over the functionally complete language. Take |$\tau :\mathsf{Form}\,{\mathcal{L}}^{b}_\Diamond \rightarrow \mathsf{Form}\,{\mathcal{L}}^{b}_\Box $| to be a translation which replaces every occurrence of |$\Diamond $| in a formula with |$\neg _{b}\Box \neg _{b}$|⁠.

From this we easily get the following:

To summarize, there is no need to define an independent theory of weak possibility as long as we work over the functionally complete language. Similarly, one could define weak impossibility as |$ \Box \neg _{b}\varphi $| and weak unnecessity as |$ \neg _{b}\Box \varphi $|⁠. In this sense, |$\mathsf{WBK}^{b}$| behaves more like classical modal logic except with strong implication in place of classical implication and Boolean negation in place of the usual classical negation.

Turns out, a lot more modalities can be expressed in |$\mathsf{WBK}^{b}$|⁠, including those of |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠, the latter being especially curious given that |$\mathsf{MBL}$| is an axiomatic extension of |$\mathsf{WBK}^{b}$|⁠.

First, observe that for every valuation |$ {\mathbb{V}} $| over a |$ \mathsf{WBK}^{b} $|-frame |$ {\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| and |$ x\in W $|⁠:

Then consider |$ {-}\Box ({-}\varphi \vee \mathsf{n}) $|⁠. We have

Observe that the last condition coincides with |$(\Box ^{-}{:}\mathsf{MBL})$|⁠. Given that |$(\Box ^{+}{:}\mathsf{MBL})$| and |$(\Box ^{+}{:}\mathsf{WBK}^{b})$| are already essentially the same, this implies that taking (where |$C $| is the combinator connective)

will give us a connective semantically indistinguishable from |$ \Box $| in |$ \mathsf{MBL} $|⁠. Then define |$\tau _{m}:\mathsf{Form}\,{\mathcal{L}}^{b}_\Box \rightarrow \mathsf{Form}\,{\mathcal{L}}^{b}_\Box $| to be a translation, which replaces every occurrence of |$\Box $| with |$\Box _{m}$| (as defined above). The following is routine given the considerations above:

As before, from this one can easily infer

Finally, we can do the same with the modal operator of |$\mathsf{BK}$| (in fact, even the modalities of the system |$\mathsf{BK}^{\mathsf{FS}}$| [27] can be defined, although we will not outline this here to save space on introducing the system). Put:

Then for any valuation |${\mathbb{V}}$| over a |$\mathsf{WBK}^{b}$|-frame |${\mathcal{W}}=\langle W,{\mathbb{R}}^{+},{\mathbb{R}}^{-}\rangle $| and |$x\in W$| we have:

It is easy to see that the resulting conditions are notational variants of |$(\Box ^{+}{:}\mathsf{BK})$| and |$(\Box ^{-}{:}\mathsf{BK})$|⁠, respectively. As before, take |$\tau _{b}:\mathsf{Form}\,{\mathcal{L}}^{n}_\Box \rightarrow \mathsf{Form}\,{\mathcal{L}}^{b}_\Box $| to be a translation, which replaces every occurrence of |$\Box $| (of a formula in the smaller language) with |$\Box _{b}$|⁠. Then

To summarize we have effectively shown that |$\mathsf{BK}$| and |$\mathsf{MBL}$| can be treated as definable fragments of |$\mathsf{WBK}^{b}$|⁠.

6 Further research

In this paper, we developed a new four-valued modal logic that gives rise to a minimal semantic framework which, in particular, generalizes that of |$\mathsf{BK}$| and |$\mathsf{MBL}$|⁠. Naturally, continued investigation of this system itself is of interest. Note that modal axioms and rule of |$\mathsf{WBK}$| rely essentially both on the verification and on the falsification conditions of implication (given that strong implication is heavily featured). This suggests that analogous but different frameworks could be developed by varying the implication connective of the systems. We already mentioned the possibility of considering Boolean implication defined as |$\varphi \supset \psi :=\neg _{b}\varphi \vee \psi $|⁠. Other natural candidates include going connexive by using implication of |$\mathsf{MC}$| (e.g. [32]), dropping Pearce’s law and using implication of |$\mathsf{N4}^{\mathsf{f}}$| or doing both by considering implication of |$\mathsf{C}$|⁠. Yet another involves getting rid of implication entirely to consider implication-free modal logics in the vein of [16].

Footnotes

References