Two variants of noncontingency operator

TL;DR

This paper introduces two variants of the noncontingency operator with distinct semantics, analyzes their expressiveness over different classes of models, and provides axiomatizations and completeness results for these modal logics.

Contribution

It defines and compares two variants of the noncontingency operator, explores their expressiveness and frame definability, and develops axiomatizations with completeness proofs.

Findings

$oxdot$-logic is less expressive than $oxplus$-logic on certain model classes.

Axiomatizations for $oxplus$ and $oxdot$ are provided over various frame classes.

Completeness is established using $oxdot$-morphisms for serial and symmetric frames.

Abstract

By slightly adapting two equivalent semantics of noncontingency operator, we obtain two variants, $\boxdot$ and $\boxplus$, with non-equivalent semantics. We show that on the class of models satisfying any of five basic properties (i.e. seriality, reflexivity, transitivity, symmetry, Euclidicity), the logic $\mathcal{L}(\boxdot)$, which has $\boxdot$ as the sole modal primitive, is less expressive than the logic $\mathcal{L}(\boxplus)$, which has $\boxplus$ as the sole modal primitive. We investigate the frame definability of both languages. We then axiomatize $\mathcal{L}(\boxplus)$ and $\mathcal{L}(\boxdot)$ over various classes of bimodal frames. Among other results, a notion of morphisms, called `$\boxdot$-morphisms', are provided to show the completeness of axiomatizations of $\mathcal{L}(\boxdot)$ over serial frames and also over symmetric frames.

Equations

$$\begin{array}[]{lclr}\mathcal{M},s\vDash\Delta\varphi&\Longleftrightarrow&\text{for all }t,u\in S,\text{ if }sRt\text{ and }sRu,&\\ &&\text{then }(\mathcal{M},t\vDash\varphi\Longleftrightarrow\mathcal{M},u\vDash\varphi).&(\text{DEF~{}1})\\ \end{array}$$

$$\begin{array}[]{lclr}\mathcal{M},s\vDash\Delta\varphi&\Longleftrightarrow&R(s)\vDash\varphi\text{ or }R(s)\vDash\neg\varphi,&(\text{DEF~{}2})\\ \end{array}$$

$$\begin{array}[]{lclr}\mathcal{M},s\vDash\boxdot\varphi&\Longleftrightarrow&\text{for all }t,u,\text{ if }sR_{1}t\text{ and }sR_{2}u,&\\ &&\text{then }(\mathcal{M},t\vDash\varphi\Longleftrightarrow\mathcal{M},u\vDash\varphi).&(\text{DEF~{}1'})\\ \mathcal{M},s\vDash\boxplus\varphi&\Longleftrightarrow&R_{1}(s)\vDash\varphi\text{ or }R_{2}(s)\vDash\neg\varphi.&(\text{DEF~{}2'})\\ \end{array}$$

$$\begin{array}[]{ll}\mathcal{L}(\boxdot):&\varphi::=p\mid\neg\varphi\mid(\varphi\land\varphi)\mid\boxdot\varphi\\ \mathcal{L}(\boxplus):&\varphi::=p\mid\neg\varphi\mid(\varphi\land\varphi)\mid\boxplus\varphi\\ \end{array}$$

$$\begin{array}[]{|lll|}\hline\cr\mathcal{M},s\vDash p&\Longleftrightarrow&s\in V(p)\\ \mathcal{M},s\vDash\neg\varphi&\Longleftrightarrow&\mathcal{M},s\nvDash\varphi\\ \mathcal{M},s\vDash\varphi\land\psi&\Longleftrightarrow&\mathcal{M},s\vDash\varphi\text{ and }\mathcal{M},s\vDash\psi\\ \mathcal{M},s\vDash\boxdot\varphi&\Longleftrightarrow&\text{for all }t,u,\text{ if }sR_{1}t\text{ and }sR_{2}u,\\ &&\text{then }(\mathcal{M},t\vDash\varphi\Longleftrightarrow\mathcal{M},u\vDash\varphi)\\ \mathcal{M},s\vDash\boxplus\varphi&\Longleftrightarrow&R_{1}(s)\vDash\varphi\text{ or }R_{2}(s)\vDash\neg\varphi\\ \hline\cr\end{array}$$

$$\begin{array}[]{lll}\mathcal{M},s\vDash\boxdot\varphi&\Longleftrightarrow&(R_{1}(s)\vDash\varphi\text{ or }R_{2}(s)\vDash\neg\varphi)\text{ and}\\ &&(R_{1}(s)\vDash\neg\varphi\text{ or }R_{2}(s)\vDash\varphi).\\ \end{array}$$

$$\begin{array}[]{lll}\mathcal{M},s\vDash\boxdot\varphi&\Longleftrightarrow&(R_{1}(s)\vDash\varphi\text{ and }R_{2}(s)\vDash\varphi)\text{ or }(R_{1}(s)\vDash\neg\varphi\text{ and }R_{2}(s)\vDash\neg\varphi).\\ \end{array}$$

$$\mathcal{M}$$

$$\begin{array}[]{ll}&\mathcal{M},s\vDash\boxdot\varphi\\ \Longleftrightarrow&(\mathcal{M},t\vDash\varphi\Longleftrightarrow\mathcal{M},u\vDash\varphi)\\ \stackrel{{\scriptstyle(\ast)}}{{\Longleftrightarrow}}&(\mathcal{M}^{\prime},u^{\prime}\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},t^{\prime}\vDash\varphi)\\ \Longleftrightarrow&\mathcal{M}^{\prime},s^{\prime}\vDash\boxdot\varphi,\\ \end{array}$$

$$\mathcal{M}$$

$$\begin{array}[]{ll}&\mathcal{M},s\vDash\boxdot\varphi\\ \Longleftrightarrow&(\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M},t\vDash\varphi)\text{ and }(\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M},u\vDash\varphi)\text{ and }(\mathcal{M},t\vDash\varphi\Longleftrightarrow\mathcal{M},u\vDash\varphi)\\ \stackrel{{\scriptstyle(\ast)}}{{\Longleftrightarrow}}&(\mathcal{M}^{\prime},s^{\prime}\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},u^{\prime}\vDash\varphi)\text{ and }(\mathcal{M},s^{\prime}\vDash\varphi\Longleftrightarrow\mathcal{M},t^{\prime}\vDash\varphi)\text{ and }(\mathcal{M}^{\prime},u^{\prime}\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},t^{\prime}\vDash\varphi)\\ \Longleftrightarrow&\mathcal{M}^{\prime},s^{\prime}\vDash\boxdot\varphi,\\ \end{array}$$

$$\mathcal{M}$$

$$\mathcal{M},x\models \phi ⟺{\mathcal{M}}^{\prime },f(x)\models \phi .$$

$$\mathcal{F}\models \phi ⟺{\mathcal{F}}^{\prime }\models \phi .$$

$$\mathcal{F}:$$

$$\begin{array}[]{lll}\text{PC}&&\text{all instances of propositional tautologies}\\ \text{CON}\boxplus&&\boxplus\varphi\land\boxplus\psi\to\boxplus(\varphi\land\psi)\land\boxplus(\varphi\vee\psi)\\ \text{DIS}\boxplus&&\boxplus\varphi\to\boxplus(\varphi\vee\psi)\vee\boxplus(\varphi\land\chi)\\ \text{MP}&&\dfrac{\varphi,\varphi\to\psi}{\psi}\\ \text{RN}\boxplus&&\dfrac{\varphi}{\boxplus\varphi\land\boxplus\neg\varphi}\\ \text{RE}\boxplus&&\dfrac{\varphi\leftrightarrow\psi}{\boxplus\varphi\leftrightarrow\boxplus\psi}\\ \end{array}$$

$$t:\overline{p}q$$

$$\phi \in s⟺{\mathcal{M}}^c,s\models \phi .$$

$$\begin{array}[]{ll}\text{PC}&\text{All instances of propositional tautologies}\\ \boxdot\text{T}&\boxdot\top\\ \boxdot\text{EQU}&\boxdot\varphi\leftrightarrow\boxdot\neg\varphi\\ \boxdot\text{CON}&\boxdot\varphi\land\boxdot\psi\to\boxdot(\varphi\land\psi)\\ \boxdot\text{DIS}&\boxdot\varphi\to\boxdot(\varphi\vee\psi)\vee\boxdot(\neg\varphi\vee\chi)\\ \text{MP}&\dfrac{\varphi~{}~{}~{}\varphi\to\psi}{\psi}\\ \text{RE}\boxdot&\dfrac{\varphi\leftrightarrow\psi}{\boxdot\varphi\leftrightarrow\boxdot\psi}\\ \end{array}$$

$${\mathcal{M}}^c,s\models \phi \text{ iff }\phi \in s.$$

$$\begin{array}[]{|llll|}\hline\cr\text{Notation}&\text{Axioms}&\text{Systems}&\text{Properties}\\ \hline\cr\hline\cr&&{\bf K^{\boxdot}}&\text{seriality}\\ \hline\cr\boxdot\text{T}&\varphi\to[\boxdot\varphi\to(\boxdot(\varphi\to\psi)\to\boxdot\psi)]&{\bf T^{\boxdot}}={\bf K^{\boxdot}}+\boxdot\text{T}&\text{reflexivity}\\ \boxdot\text{B}&\varphi\to\boxdot((\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi)&{\bf B^{\boxdot}}={\bf K^{\boxdot}}+\boxdot\text{B}&\text{symmetry}\\ \boxdot 4&\boxdot\varphi\to\boxdot(\boxdot\varphi\vee\psi)&{\bf K4^{\boxdot}}={\bf K^{\boxdot}}+\boxdot 4&qt\&pt\\ \boxdot 5&\neg\boxdot\varphi\to\boxdot(\neg\boxdot\varphi\vee\psi)&{\bf K5^{\boxdot}}={\bf K^{\boxdot}}+\boxdot 5&qe\&pe\\ \hline\cr\end{array}$$

$$u\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\mathcal{M}}^{\prime },s\models \phi ⟺\mathcal{M},g(s)\models \phi .$$

$$\phi \in s\text{ iff }{\mathcal{M}}^r,s\models \phi .$$

$$\mathcal{M}$$

$$T_1=\{t\in S\mid s{R}_{1}t\text{ for some }s\in S,\text{ and }t{R}_{1}u\text{ for no }u\in S,\text{ and }t{R}_{2}v\text{ for no }v\in S\},$$

$$T_2=\{t\in S\mid s{R}_{2}t\text{ for some }s\in S,\text{ and }t{R}_{1}u\text{ for no }u\in S,\text{ and }t{R}_{2}v\text{ for no }v\in S\},$$

$${\mathcal{M}}^{+},s\models \phi ⟺\mathcal{M},h(s)\models \phi .$$

$$t:p$$

Full text

1 Introduction

Past decades have witnessed a bunch of studies on noncontingency logic, see e.g. [Hum95, Kuh95, Zol99, vdHL04, Ste08, FWvD14, FvD15, FWvD15, Fan18a, Fan18b, Fan19]. This logic is obtained by enriching propositional logic with an important metaphysical notion — contingency, which dates back to Aristotle [Bro67]. Intuitively, a proposition is contingent, if it is possibly true and also possibly false; otherwise, it is noncontingent, i.e. necessarily true or necessarily false. In an epistemic setting, contingency amounts to ‘ignorance’, and noncontingency amounts to ‘knowing whether’, which is perhaps the closest knowing-wh companion to ‘knowing that’ (namely, standard propositional knowledge) among various knowledge types [Wan16].

Formally, given a Kripke model $\mathcal{M}=\langle S,R,V\rangle$, where $S$ is a nonempty set of possible worlds, $R\subseteq S\times S$ is called accessibility relation, and $V$ is a valuation that assigns a set $V(p)\subseteq S$ to each propositional variable $p$, the formula $\Delta\varphi$, read “it is noncontingent that $\varphi$”, is evaluated as follows:

[TABLE]

Equivalently,

[TABLE]

where $R(s)\vDash\varphi$ means that $\varphi$ is true at all successors of $s$ w.r.t. $R$, and similarly for $R(s)\vDash\neg\varphi$.

By slightly adapting the above semantics, we obtain two variants of $\Delta$, denoted $\boxdot$ and $\boxplus$ respectively, as follows.

[TABLE]

It is not hard to see that (DEF 1) and (DEF 2) are, respectively, special cases of (DEF 1’) and (DEF 2’) when $R_{1}=R_{2}=R$. This entails that both $\boxdot$ and $\boxplus$ are more general than $\Delta$. Moreover, as $\vDash\boxdot\varphi\leftrightarrow\boxdot\neg\varphi$ but $\nvDash\boxplus\varphi\leftrightarrow\boxplus\neg\varphi$ (as we will see below), we may call $\boxdot$ ‘general noncontingency’ and $\boxplus$ ‘pseudo noncontingency’ operators. Unlike the fact that (DEF 1) is equivalent to (DEF 2), (DEF 1’) and (DEF 2’) are not equivalent, that is, $\nvDash\boxdot\varphi\leftrightarrow\boxplus\varphi$.

This paper investigates both operators. Roughly speaking, a proposition is generalized noncontingent, if the proposition has the same truth value no matter whether you look at it in this way ($R_{1}$) or in that way ($R_{2}$); and a proposition is pseudo noncontingent, if it is necessary in this way ($R_{1}$), or it is impossible in that way ($R_{2}$). Whenever both ways are the same, both operators then become the more-familiar noncontingency operator.

The remainder of the paper is structured as follows. After introducing the syntax and semantics of logic $\mathcal{L}(\boxdot)$ for generalized noncontingency and logic $\mathcal{L}(\boxplus)$ for pseudo noncontingency (Sec. 2), we compare the relative expressivity of the two logics (Sec. 3), and investigate their frame definability (Sec. 5) with the help of a notion of $\boxdot$-morphisms (Sec. 4). We then axiomatize $\mathcal{L}(\boxplus)$ and $\mathcal{L}(\boxdot)$ over various bimodal frames in Sec. 6 and Sec. 7, where the completeness of $\mathcal{L}(\boxdot)$ over serial frames and also over symmetric frames are proved via the notion of $\boxdot$-morphisms. We conclude with a few future work in Sec. 8.

2 Syntax and semantics

Let P be a fixed nonempty set of propositional variables.

Definition 1** (Syntax).**

Where $p\in\textbf{P}$, the language $\mathcal{L}(\boxdot)$ of generalized noncontingency logic and the language $\mathcal{L}(\boxplus)$ of pseudo noncontingency logic are defined inductively as follows.

[TABLE]

$\boxdot\varphi$ and $\boxplus\varphi$ are read “it is generalized noncontingent that $\varphi$” and “it is pseudo noncontingent that $\varphi$”, respectively. As we will see below, the comparisons between the two languages are interesting, both in expressivity and in axiomatizations.

The languages are interpreted on bimodal models. To say that $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ is a bimodal model, if $S$ is a nonempty set of possible worlds, $R_{1}$ and $R_{2}$ are accessibility relations over $S$, and $V$ is a function assigning to each propositional variable a subset of $S$. A bimodal frame $\mathcal{F}$ is a bimodal model without valuations. If $R_{1}$ and $R_{2}$ both possess a property $P$ (such as seriality, reflexivity, transitivity, symmetry, Euclidicity), then $\mathcal{M}$ ($\mathcal{F}$) is called a $P$ bimodal model (resp. a $P$ bimodal frame). Moreover, $R_{i}(s)=\{t\in S\mid sR_{i}t\}$ for $i=1,2$.

Definition 2** (Semantics).**

Given a bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ and $s\in S$, the semantics of both languages is defined as follows.

[TABLE]

Where for $i\in\{1,2\}$, $R_{i}(s)\vDash\varphi$ stands for “for all $t\in R_{i}(s),\mathcal{M},t\vDash\varphi$”, and $R_{i}(s)\nvDash\varphi$ for the negation of this claim, that is, “for some $t\in R_{i}(s)$, $\mathcal{M},t\nvDash\varphi$”. Obviously, when $R_{1}(s)=\emptyset$ or $R_{2}(s)=\emptyset$, it holds vacuously that $\mathcal{M},s\vDash\boxplus\varphi$ and $\mathcal{M},s\vDash\boxdot\varphi$ for all $\varphi$; if $R_{1}=R_{2}$, then $\boxplus=\boxdot$ and each of them becomes an operator for noncontingency.

It is noteworthy remarking that $\vDash\boxdot\varphi\leftrightarrow(\boxplus\varphi\land\boxplus\neg\varphi)$, as can be seen more clearly from an alternative semantical definition for $\boxdot$.

[TABLE]

Consequently, $\boxplus$ is deductively weaker than $\boxdot$. In contrast, as Sec. 3 will show, $\boxplus$ is deductively stronger than $\boxdot$, equivalently, $\boxdot$ is expressively weaker than $\boxplus$.111As for the definitions of ‘deductively weaker’ and ‘expressively weaker’, we refer to [Fan17].

Note that $\nvDash\boxplus\varphi\leftrightarrow\boxplus\neg\varphi$ but $\vDash\boxdot\varphi\leftrightarrow\boxdot\neg\varphi$. To see the former, consider a model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ in which $S=\{s,t,u\}$, $R_{1}(s)=\{t\}$ and $R_{2}(s)=\{u\}$, and $V(p)=\{t\}$. Then it should be easily verified that $s\vDash\boxplus p$ but $s\nvDash\boxplus\neg p$. This will matter when we look into the differences between axiomatizations of $\boxplus$-logics and of $\boxdot$-logics.

We may define $\mathcal{M},s\vDash\Box_{i}\varphi$ as $R_{i}(s)\vDash\varphi$, where $i\in\{1,2\}$, then $\boxplus\varphi$ is equivalent to $\Box_{1}\varphi\vee\Box_{2}\neg\varphi$. The operator $\boxplus$, written $N^{\prime\prime\prime}$ on  [Hum16, p. 229], to our knowledge, has not been axiomatized in the literature.

If we read $\Box_{i}\varphi$ as “the agent $i$ believes that $\varphi$”, then it is not hard to see that the negation of $\boxdot$ characterizes the notion of weak belief-disagreement in [CP18]: one agent fails to believe one proposition and the other fails to believe its negation. In that paper, the notion is mentioned in passing only, which is based on serial bimodal frames.

On serial bimodal frames, the semantics of $\boxdot$ is equivalent to

[TABLE]

The epistemic meaning of this definition is that agents 1 and 2 have the same knowledge about $\varphi$, i.e. they both know $\varphi$, or they both know $\neg\varphi$; in a doxastic reading, it means ‘agents 1 and 2 have the belief agreement on $\varphi$’.

To simplify the proofs later, we claim the following results, which should be easily verified.

Proposition 3**.**

Let $i,j\in\{1,2\}$ and $i\neq j$ and $R_{j}(s)\neq\emptyset$. If $\mathcal{M},s\vDash\boxdot\varphi$, then $\mathcal{M},s\vDash\Delta_{i}\varphi$.

Note that the converse fails. For example, in a model $\mathcal{M}$, $s$ has only a single $R_{i}$-successor $t$, and another single $R_{j}$-successor $u$, whereas $t$ and $u$ have different truth values for $\varphi$. In spite of this, the converse indeed holds when $R_{i}(s)$ and $R_{j}(s)$ has a common element.

Proposition 4**.**

Suppose that $R_{1}(s)\cap R_{2}(s)\neq\emptyset$. If $\mathcal{M},s\vDash\Delta_{1}\varphi\land\Delta_{2}\varphi$, then $\mathcal{M},s\vDash\boxdot\varphi$.

Corollary 5**.**

Suppose that $R_{1}(s)\cap R_{2}(s)\neq\emptyset$. Then $\mathcal{M},s\vDash\Delta_{1}\varphi\land\Delta_{2}\varphi$ iff $\mathcal{M},s\vDash\boxdot\varphi$.

3 Expressivity

This section compares the relative expressivity of $\mathcal{L}(\boxdot)$ and $\mathcal{L}(\boxplus)$. It turns out that the former is less expressive than the latter on all five classes of basic bimodal models.

To make our presentation self-contained, we introduce some necessary technical terms.

Definition 6**.**

Let $\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ be two languages that are interpreted on the same class of models $\mathbb{C}$.

• •

$\mathcal{L}_{2}$ is at least as expressive as $\mathcal{L}_{1}$, notation: $\mathcal{L}_{1}\preceq\mathcal{L}_{2}$, if for all $\varphi\in\mathcal{L}_{1}$, there exists $\psi\in\mathcal{L}_{2}$ such that for all $\mathcal{M}$ in $\mathbb{C}$ and all $s$ in $\mathcal{M}$, we have that $\mathcal{M},s\vDash\varphi$ iff $\mathcal{M},s\vDash\psi$.

• •

$\mathcal{L}_{1}$ and $\mathcal{L}_{2}$ are equally expressive, notation: $\mathcal{L}_{1}\equiv\mathcal{L}_{2}$, if $\mathcal{L}_{1}\preceq\mathcal{L}_{2}$ and $\mathcal{L}_{2}\preceq\mathcal{L}_{1}$.

• •

$\mathcal{L}_{1}$ is less expressive than $\mathcal{L}_{2}$, notation: $\mathcal{L}_{1}\prec\mathcal{L}_{2}$, if $\mathcal{L}_{1}\preceq\mathcal{L}_{2}$ but $\mathcal{L}_{2}\not\preceq\mathcal{L}_{1}$.

Proposition 7**.**

$\mathcal{L}(\boxdot)$ is less expressive than $\mathcal{L}(\boxplus)$ on the class of all bimodal models, the class of serial bimodal models, the class of transitive bimodal models, the class of Euclidean bimodal models.

Proof.

We have already seen that $\boxdot$ is definable in $\mathcal{L}(\boxplus)$, as $\vDash\boxdot\varphi\leftrightarrow\boxplus\varphi\land\boxplus\neg\varphi$. This entails that $\mathcal{L}(\boxdot)\preceq\mathcal{L}(\boxplus)$.

To show $\mathcal{L}(\boxplus)\not\preceq\mathcal{L}(\boxdot)$, consider the following serial, transitive, Euclidean bimodal models:

[TABLE]

One can check that $\mathcal{M},s\vDash\boxplus p$ and $\mathcal{M}^{\prime},s^{\prime}\nvDash\boxplus p$, thus the $\mathcal{L}(\boxplus)$-formula $\boxplus p$ can distinguish $(\mathcal{M},s)$ and $(\mathcal{M}^{\prime},s^{\prime})$.

However, $(\mathcal{M},s)$ and $(\mathcal{M}^{\prime},s^{\prime})$ cannot be distinguished by any $\mathcal{L}(\boxdot)$-formula. That is, for all $\varphi\in\mathcal{L}(\boxdot)$, we have $(\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},s^{\prime}\vDash\varphi)$. The proof proceeds by induction on $\varphi$.

The base case and Boolean cases are straightforward. For the case $\boxdot\varphi$, we have

[TABLE]

where $(\ast)$ holds since $\mathcal{M},t\vDash\varphi$ iff $\mathcal{M}^{\prime},u^{\prime}\vDash\varphi$, and $\mathcal{M},u\vDash\varphi$ iff $\mathcal{M}^{\prime},t^{\prime}\vDash\varphi$ for all $\varphi\in\mathcal{L}(\boxdot)$, as can be easily verified.

∎

Proposition 8**.**

$\mathcal{L}(\boxdot)$ is less expressive than $\mathcal{L}(\boxplus)$ on the class of symmetric bimodal models.

Proof.

Again, $\mathcal{L}(\boxdot)\preceq\mathcal{L}(\boxplus)$. For the strict part, consider the following symmetric bimodal models:

[TABLE]

First, $\mathcal{M},s\vDash\boxplus p$ but $\mathcal{M}^{\prime},s^{\prime}\nvDash\boxplus p$. This means that $(\mathcal{M},s)$ and $(\mathcal{M}^{\prime},s^{\prime})$ can be distinguished by $\mathcal{L}(\boxplus)$.

Second, as shown in Prop. 7, we can prove that for all $\varphi\in\mathcal{L}(\boxdot)$, $\mathcal{M},s\vDash\varphi$ iff $\mathcal{M}^{\prime},s^{\prime}\vDash\varphi$. Then $(\mathcal{M},s)$ and $(\mathcal{M}^{\prime},s^{\prime})$ cannot be distinguished by $\mathcal{L}(\boxdot)$. ∎

Proposition 9**.**

$\mathcal{L}(\boxdot)$ is less expressive than $\mathcal{L}(\boxplus)$ on the class of reflexive bimodal models.

Proof.

Again, $\mathcal{L}(\boxdot)\preceq\mathcal{L}(\boxplus)$.

For the strict part, consider the following reflexive bimodal models:

[TABLE]

First, $\mathcal{M},s\vDash\boxplus p$ but $\mathcal{M}^{\prime},s^{\prime}\nvDash\boxplus p$, thus $\boxplus p$ can distinguish $(\mathcal{M},s)$ and $(\mathcal{M}^{\prime},s^{\prime})$.

However, no $\mathcal{L}(\boxdot)$-formula can distinguish both pointed models. That is, for all $\varphi\in\mathcal{L}(\boxdot)$, we have $(\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},s^{\prime}\vDash\varphi)$. The proof proceeds with induction on $\varphi$. We only consider the nontrivial case $\boxdot\varphi$.

[TABLE]

where $(\ast)$ is the case due to the induction hypothesis that $\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},s^{\prime}\vDash\varphi$, and the fact that $\mathcal{M},t\vDash\varphi$ iff $\mathcal{M}^{\prime},u^{\prime}\vDash\varphi$, and $\mathcal{M},u\vDash\varphi$ iff $\mathcal{M}^{\prime},t^{\prime}\vDash\varphi$ for all $\varphi\in\mathcal{L}(\boxdot)$, as can be easily verified.

∎

Remark 10**.**

Note that in the proof of Prop. 9, $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are both serial and transitive, but not Euclidean; for instance, $sR_{1}t$ and $sR_{1}s$ but not $tR_{1}s$, thus Prop. 7 cannot be shown by using the constructed models in Prop. 9.

The clear-sighted reader may ask whether the Euclidean closures of $\mathcal{M}$ and $\mathcal{M}^{\prime}$ in Prop. 9 can handle Prop. 7 (and even Prop. 8) uniformly. That is, if we construct models $\mathcal{M}$ and $\mathcal{M}^{\prime}$ as follows:

[TABLE]

then does $\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},s^{\prime}\vDash\varphi$ hold for all $\varphi\in\mathcal{L}(\boxdot)$?

The answer seems negative. The reason is as follows: to show the case $\boxdot\varphi$, that is, $\mathcal{M},s\vDash\boxdot\varphi\Longleftrightarrow\mathcal{M}^{\prime},s^{\prime}\vDash\boxdot\varphi$, (as before) we need to prove that $\mathcal{M},t\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},u^{\prime}\vDash\varphi$ for all $\varphi\in\mathcal{L}(\boxdot)$ (and also $\mathcal{M},u\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},t^{\prime}\vDash\varphi$ for all $\varphi\in\mathcal{L}(\boxdot)$), whose case $\boxdot\varphi$ relies on showing again that $\mathcal{M},s\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},s^{\prime}\vDash\varphi$ for all $\varphi\in\mathcal{L}(\boxdot)$. This is a vicious circle.

In comparison, this situation does not occur in the proofs of Prop. 7-Prop. 9; instead, as any point $x\in\{t,u,t^{\prime},u^{\prime}\}$ in the proofs of those propositions has no two different successors with respect to $R_{1}$ and $R_{2}$, all formulas of the form $\boxdot\varphi$ are true at $x$.

4 $\boxdot$-morphisms

In this section, we introduce a notion of $\boxdot$-morphisms, which is useful in the proof of frame undefinability and the completeness proof of $\mathcal{L}(\boxdot)$ over serial frames and also over symmetric frames below.

Definition 11**.**

Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ and $\mathcal{M}^{\prime}=\langle S^{\prime},R_{1}^{\prime},R_{2}^{\prime},V^{\prime}\rangle$ be two bimodal models. A function $f:S\to S^{\prime}$ is a $\boxdot$-morphism from $\mathcal{M}$ to $\mathcal{M}^{\prime}$, if for all $x\in S$,

• (Var)

For all $p\in\textbf{P}$, $x\in V(p)$ iff $f(x)\in V^{\prime}(p)$,

• (Forth)

For any $y,z\in S$, if $xR_{1}y$ and $xR_{2}z$ and $f(y)\neq f(z)$, then $f(x)R_{1}^{\prime}f(y)$ and $f(x)R_{2}^{\prime}f(z)$,

• (Back)

For all $y^{\prime},z^{\prime}\in S^{\prime}$, if $f(x)R_{1}^{\prime}y^{\prime}$ and $f(x)R_{2}^{\prime}z^{\prime}$ and $y^{\prime}\neq z^{\prime}$, then there are $y,z\in S$ such that $xR_{1}y$ and $xR_{2}z$ and $f(y)=y^{\prime}$ and $f(z)=z^{\prime}$.

We say that $\mathcal{M}^{\prime}$ is a $\boxdot$-morphic image of $\mathcal{M}$, if there is a surjective $\boxdot$-morphism from $\mathcal{M}$ to $\mathcal{M}^{\prime}$.

The following result indicates that $\mathcal{L}(\boxdot)$-formulas and $\mathcal{L}(\boxplus)$-formulas are invariant under $\boxdot$-morphisms.

Proposition 12**.**

Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ and $\mathcal{M}^{\prime}=\langle S^{\prime},R_{1}^{\prime},R_{2}^{\prime},V^{\prime}\rangle$ be two bimodal models, and let $f$ be a $\boxdot$-morphism from $\mathcal{M}$ to $\mathcal{M}^{\prime}$. Then for all $x\in S$, for all $\varphi\in\mathcal{L}(\boxdot)\cup\mathcal{L}(\boxplus)$, we have

[TABLE]

Proof.

By induction on $\varphi\in\mathcal{L}(\boxdot)\cup\mathcal{L}(\boxplus)$. We only consider the nontrivial case $\boxdot\varphi$ and $\boxplus\varphi$.

Suppose that $\mathcal{M},x\nvDash\boxdot\varphi$, to show that $\mathcal{M}^{\prime},f(x)\nvDash\boxdot\varphi$. By supposition, there are $y,z\in S$ such that $xR_{1}y$ and $xR_{2}z$ and it is not the case that $(\mathcal{M},y\vDash\varphi\Longleftrightarrow\mathcal{M},z\vDash\varphi)$. By induction hypothesis, it is not the case that $(\mathcal{M}^{\prime},f(y)\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},f(z)\vDash\varphi)$, which implies that $f(y)\neq f(z)$. Now using (Forth), we obtain $f(x)R^{\prime}_{1}f(y)$ and $f(x)R^{\prime}_{2}f(z)$. Therefore, $\mathcal{M}^{\prime},f(x)\nvDash\boxdot\varphi$.

Conversely, assume that $\mathcal{M}^{\prime},f(x)\nvDash\boxdot\varphi$, to prove that $\mathcal{M},x\nvDash\boxdot\varphi$. By assumption, there exist $y^{\prime},z^{\prime}\in S^{\prime}$ such that $f(x)R_{1}^{\prime}y^{\prime}$ and $f(x)R_{2}^{\prime}z^{\prime}$ and it is not the case that $(\mathcal{M}^{\prime},y^{\prime}\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},z^{\prime}\vDash\varphi)$. It is clear that $y^{\prime}\neq z^{\prime}$. Using (Back), we infer that there are $y,z\in S$ such that $xR_{1}y$ and $xR_{2}z$ and $f(y)=y^{\prime}$ and $f(z)=z^{\prime}$, and thus it is not the case that $(\mathcal{M}^{\prime},f(y)\vDash\varphi\Longleftrightarrow\mathcal{M}^{\prime},f(z)\vDash\varphi)$. By induction hypothesis, it is not the case that $(\mathcal{M},y\vDash\varphi\Longleftrightarrow\mathcal{M},z\vDash\varphi)$. Therefore, $\mathcal{M},x\nvDash\boxdot\varphi$.

Suppose that $\mathcal{M},x\nvDash\boxplus\varphi$, to prove that $\mathcal{M}^{\prime},f(x)\nvDash\boxplus\varphi$. By supposition, there exists $y\in S$ such that $xR_{1}y$ and $\mathcal{M},y\nvDash\varphi$, and there exists $z\in S$ such that $xR_{2}z$ and $\mathcal{M},z\nvDash\neg\varphi$ (viz. $\mathcal{M},z\vDash\varphi$). By induction hypothesis, $\mathcal{M}^{\prime},f(y)\nvDash\varphi$ and $\mathcal{M}^{\prime},f(z)\vDash\varphi$, which implies that $f(y)\neq f(z)$. Then applying (Forth), we infer that $f(x)R_{1}^{\prime}f(y)$ and $f(x)R_{2}^{\prime}f(z)$. Therefore, $\mathcal{M}^{\prime},f(x)\nvDash\boxplus\varphi$.

Conversely, assume that $\mathcal{M}^{\prime},f(x)\nvDash\boxplus\varphi$, to demonstrate that $\mathcal{M},x\nvDash\boxdot\varphi$. By assumption, there is a $y^{\prime}\in S^{\prime}$ such that $f(x)R_{1}^{\prime}y^{\prime}$ and $\mathcal{M}^{\prime},y^{\prime}\nvDash\varphi$, and there is a $z^{\prime}\in S^{\prime}$ such that $f(x)R_{2}^{\prime}z^{\prime}$ and $\mathcal{M}^{\prime},z^{\prime}\nvDash\neg\varphi$ (namely, $\mathcal{M}^{\prime},z^{\prime}\vDash\varphi$). Then $y^{\prime}\neq z^{\prime}$. Applying (Back), we derive that there exist $y,z\in S$ such that $xR_{1}y$ and $xR_{2}z$ and $f(y)=y^{\prime}$ and $f(z)=z^{\prime}$. Thus $\mathcal{M}^{\prime},f(y)\nvDash\varphi$ and $\mathcal{M}^{\prime},f(z)\vDash\varphi$. By induction hypothesis, $\mathcal{M},y\nvDash\varphi$ and $\mathcal{M},z\vDash\varphi$, and therefore $\mathcal{M},x\nvDash\boxplus\varphi$, as desired. ∎

5 Frame definability

This section investigates the frame definability of logics $\mathcal{L}(\boxdot)$ and $\mathcal{L}(\boxplus)$. It turns out that all five basic frame properties, i.e. seriality, reflexivity, transitivity, symmetry, Euclidicity, are not definable in both logics. For this, we adopt the notion of $\boxdot$-morphisms on the frame level, which is obtained from Def. 11 by leaving out the valuations.

Definition 13**.**

Let $\mathcal{F}=\langle S,R_{1},R_{2}\rangle$ and $\mathcal{F}^{\prime}=\langle S^{\prime},R_{1}^{\prime},R_{2}^{\prime}\rangle$ be two bimodal frames. A function $f:S\to S^{\prime}$ is a $\boxdot$-morphism from $\mathcal{F}$ to $\mathcal{F}^{\prime}$, if for all $x\in S$,

• (Forth)

For any $y,z\in S$, if $xR_{1}y$ and $xR_{2}z$ and $f(y)\neq f(z)$, then $f(x)R_{1}^{\prime}f(y)$ and $f(x)R_{2}^{\prime}f(z)$,

• (Back)

For all $y^{\prime},z^{\prime}\in S^{\prime}$, if $f(x)R_{1}^{\prime}y^{\prime}$ and $f(x)R_{2}^{\prime}z^{\prime}$ and $y^{\prime}\neq z^{\prime}$, then there are $y,z\in S$ such that $xR_{1}y$ and $xR_{2}z$ and $f(y)=y^{\prime}$ and $f(z)=z^{\prime}$.

We say that $\mathcal{F}^{\prime}$ is a $\boxdot$-morphic image of $\mathcal{F}$, if there is a surjective $\boxdot$-morphism from $\mathcal{F}$ to $\mathcal{F}^{\prime}$.

Proposition 14**.**

Let $\mathcal{F}=\langle S,R_{1},R_{2}\rangle$ and $\mathcal{F}^{\prime}=\langle S^{\prime},R_{1}^{\prime},R_{2}^{\prime}\rangle$ be two bimodal frames. If $\mathcal{F}^{\prime}$ is a $\boxdot$-morphic image of $\mathcal{F}$, then for all $\varphi\in\mathcal{L}(\boxdot)\cup\mathcal{L}(\boxplus)$, we have

[TABLE]

Proof.

Assume that $\mathcal{F}^{\prime}$ is a $\boxdot$-morphic image of $\mathcal{F}$. Then there is a surjective $\boxdot$-morphism from $\mathcal{F}$ to $\mathcal{F}^{\prime}$, say $f$.

Suppose that $\mathcal{F}\nvDash\varphi$, to show that $\mathcal{F}^{\prime}\vDash\varphi$. By supposition, there exists a valuation $V$ on $\mathcal{F}$ and $s\in S$ such that $\langle\mathcal{F},V\rangle,s\nvDash\varphi$. Define a valuation $V^{\prime}$ on $\mathcal{F}^{\prime}$ by $V^{\prime}(p)=\{f(x)\mid x\in V(p)\}$ for all $p\in\textbf{P}$. Then $f$ is a $\boxdot$-morphism from $\langle\mathcal{F},V\rangle$ to $\langle\mathcal{F}^{\prime},V^{\prime}\rangle$. By Prop. 12 and the fact that $\langle\mathcal{F},V\rangle,s\nvDash\varphi$, we obtain $\langle\mathcal{F}^{\prime},V^{\prime}\rangle,f(s)\nvDash\varphi$, and therefore $\mathcal{F}^{\prime}\nvDash\varphi$.

Conversely, suppose that $\mathcal{F}^{\prime}\nvDash\varphi$, to show that $\mathcal{F}\nvDash\varphi$. By supposition, there is a valuation $V^{\prime}$ on $\mathcal{F}^{\prime}$ and $s^{\prime}\in S^{\prime}$ such that $\langle\mathcal{F}^{\prime},V^{\prime}\rangle,s^{\prime}\nvDash\varphi$. Since $f$ is surjective, there must be an $s\in S$ such that $s^{\prime}=f(s)$. Define a valuation $V$ on $\mathcal{F}$ by $V(p)=\{x\mid f(x)\in V^{\prime}(p)\}$ for all $p\in\textbf{P}$. Then $f$ is a $\boxdot$-morphism from $\langle\mathcal{F},V\rangle$ to $\langle\mathcal{F}^{\prime},V^{\prime}\rangle$. By Prop. 12 again and the fact that $\langle\mathcal{F}^{\prime},V^{\prime}\rangle,f(s)\nvDash\varphi$, we infer that $\langle\mathcal{F},V\rangle,s\nvDash\varphi$, and therefore $\mathcal{F}\nvDash\varphi$, as desired. ∎

Proposition 15**.**

None of seriality, reflexivity, transitivity, symmetry and Euclidicity are definable in $\mathcal{L}(\boxdot)\cup\mathcal{L}(\boxplus)$.

Proof.

Consider the following bimodal frames:

[TABLE]

Define a function $g$ from $\mathcal{F}$ to $\mathcal{F}^{\prime}$ as follows: $g(s)=g(t)=g(u)=s^{\prime}$. It is not hard to check that $g$ is a surjective $\boxdot$-morphism, thus $\mathcal{F}^{\prime}$ is a $\boxdot$-morphic image of $\mathcal{F}$. By Prop. 14, $\mathcal{F}\vDash\varphi$ iff $\mathcal{F}^{\prime}\vDash\varphi$ for all $\varphi\in\mathcal{L}(\boxdot)\cup\mathcal{L}(\boxplus)$.

If seriality were defined by a set of $\mathcal{L}(\boxdot)$-formulas or a set of $\mathcal{L}(\boxplus)$-formulas, say $\Gamma$, then as $\mathcal{F}^{\prime}$ is serial, $\mathcal{F}^{\prime}\vDash\Gamma$, and thus $\mathcal{F}\vDash\Gamma$, which would imply that $\mathcal{F}$ should be serial: a contradiction. Thus seriality is not definable in $\mathcal{L}(\boxdot)$. The proofs for the undefinability of other frame properties are analogous. ∎

The frame undefinability results can be understood in the following way: since in the figures of Prop. 15, we have $R_{1}=R_{2}$, and we already commented that if $R_{1}=R_{2}$, then each of $\boxdot$ and $\boxplus$ becomes a non-contingency operator; moreover, none of the five basic frame properties are definable in a logic with any non-contingency operator as a sole primitive modality [Zol99, FWvD15], thus Prop. 15 obtains.

6 Axiomatizations for $\mathcal{L}(\boxplus)$

This section first presents the minimal logic for $\mathcal{L}(\boxplus)$, and shows its soundness and completeness, and then demonstrates that the same logic is also sound and strongly complete with respect to the class of serial bimodal frames.

6.1 The minimal logic and soundness

Definition 16**.**

The minimal logic for $\mathcal{L}(\boxplus)$, denoted ${\bf K^{\boxplus}}$, consists of the following axioms and inference rules:

[TABLE]

Notions of deductions and theorems are defined as normal.

Recall that in the minimal noncontingency logic, the axiom $\Delta\varphi\to\Delta(\varphi\vee\psi)\vee\Delta(\varphi\land\chi)$ (denoted DIS$\Delta$ hereafter) can be replaced with the rule $\dfrac{\varphi\to\psi~{}~{}~{}\psi\to\chi}{\Delta\psi\to\Delta\varphi\vee\Delta\chi}$ [Hum02, p. 110]. This also applies to its $\boxplus$-correspondent; more precisely, the axiom DIS$\boxplus$ is replaceable with the rule $\dfrac{\varphi\to\psi~{}~{}~{}\psi\to\chi}{\boxplus\psi\to\boxplus\varphi\vee\boxplus\chi}$, given the rule RE$\boxplus$.

Also, DIS$\Delta$ can be replaced with $\Delta\varphi\to\Delta(\varphi\vee\psi)\vee\Delta(\neg\varphi\vee\chi)$ (called ‘Kuhn’s axiom’), and even with the formula (which is equivalent to Kuhn’s axiom) with less district schematic letters $\Delta\varphi\to\Delta(\varphi\vee\psi)\vee\Delta(\neg\varphi\vee\psi)$, see [Hum02, pp. 110-111]. In comparison, the axiom $\text{DIS}\boxplus$ cannot be replaced with $\boxplus\varphi\to\boxplus(\varphi\vee\psi)\vee\boxplus(\neg\varphi\vee\chi)$, neither with $\boxplus\varphi\to\boxplus(\varphi\vee\psi)\vee\boxplus(\neg\varphi\vee\psi)$, as illustrated below.

[TABLE]

On one hand, because $R_{2}(s)\vDash\neg p$, we have $s\vDash\boxplus p$. On the other hand, since $R_{1}(s)\nvDash p\vee q$ (as $sR_{1}s$ and $s\nvDash p\vee q$) and $R_{2}(s)\nvDash\neg(p\vee q)$ (as $sR_{2}t$ and $t\vDash p\vee q$), it follows that $s\nvDash\boxplus(p\vee q)$; moreover, since $R_{1}(s)\nvDash\neg p\vee q$ (as $sR_{1}u$ and $u\vDash p\land\neg q$) and $R_{2}(s)\nvDash\neg(\neg p\vee q)$ (as $sR_{2}t$ and $t\vDash\neg p\vee q$), it follows that $s\nvDash\boxplus(\neg p\vee q)$. This indicates that $\boxplus p\to\boxplus(p\vee q)\vee\boxplus(\neg p\vee q)$ is invalid.

Proposition 17**.**

${\bf K^{\boxplus}}$ is sound with respect to the class of all bimodal frames.

Proof.

We take the validity of $\text{CON}\boxplus$ and $\text{DIS}\boxplus$ as examples. Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ be an arbitrary bimodal model and $s\in S$.

Suppose that $\mathcal{M},s\vDash\boxplus\varphi\land\boxplus\psi$. Then $R_{1}(s)\vDash\varphi$ or $R_{2}(s)\vDash\neg\varphi$, and $R_{1}(s)\vDash\psi$ or $R_{2}(s)\vDash\neg\psi$.

If $R_{2}(s)\vDash\neg\varphi$ or $R_{2}(s)\vDash\neg\psi$, then $R_{2}(s)\vDash\neg(\varphi\land\psi)$; otherwise, that is, if $R_{1}(s)\vDash\varphi$ and $R_{1}(s)\vDash\psi$, then $R_{1}(s)\vDash\varphi\land\psi$. Thus either $R_{1}(s)\vDash\varphi\land\psi$ or $R_{2}(s)\vDash\neg(\varphi\land\psi)$, and therefore $\mathcal{M},s\vDash\boxplus(\varphi\land\psi)$.

If $R_{1}(s)\vDash\varphi$ or $R_{1}(s)\vDash\psi$, then $R_{1}(s)\vDash\varphi\vee\psi$; otherwise, that is, if $R_{2}(s)\vDash\neg\varphi$ and $R_{2}(s)\vDash\neg\psi$, then $R_{2}(s)\vDash\neg(\varphi\vee\psi)$. Thus either $R_{1}(s)\vDash\varphi\vee\psi$ or $R_{2}(s)\vDash\neg(\varphi\vee\psi)$, and therefore $\mathcal{M},s\vDash\boxplus(\varphi\vee\psi)$. Hitherto we have completed the validity of $\text{CON}\boxplus$.

Now suppose that $\mathcal{M},s\vDash\boxplus\varphi$, then $R_{1}(s)\vDash\varphi$ or $R_{2}(s)\vDash\neg\varphi$. If it is the case that $R_{1}(s)\vDash\varphi$, then $R_{1}(s)\vDash\varphi\vee\psi$, which implies that $\mathcal{M},s\vDash\boxplus(\varphi\vee\psi)$; if it is the case that $R_{2}(s)\vDash\neg\varphi$, then $R_{2}(s)\vDash\neg(\varphi\land\chi)$, which entails that $\mathcal{M},s\vDash\boxplus(\varphi\land\chi)$. Therefore, $\mathcal{M},s\vDash\boxplus(\varphi\vee\psi)\vee\boxplus(\varphi\land\chi)$. Hitherto we have completed the validity of $\text{DIS}\boxplus$. ∎

6.2 Completeness

This part deals with the completeness of ${\bf K^{\boxplus}}$. We adopt the standard canonical model construction. However, a tricky thing is how to define two suitable canonical relations to handle the operator $\boxplus$.

Definition 18**.**

The canonical model for ${\bf K^{\boxplus}}$ is a tuple $\mathcal{M}^{c}=\langle S^{c},R^{c}_{1},R^{c}_{2},V^{c}\rangle$, where

• •

$S^{c}=\{s\mid s\text{ is a maximal }{\bf K^{\boxplus}}\text{-consistent set}\}$;

• •

$sR^{c}_{1}t$ iff $\lambda_{1}(s)\subseteq t$, where $\lambda_{1}(s)=\{\varphi\mid\boxplus(\varphi\vee\psi)\in s\text{ for all }\psi\}$;

• •

$sR^{c}_{2}u$ iff $\lambda_{2}(s)\subseteq u$, where $\lambda_{2}(s)=\{\varphi\mid\boxplus(\neg\varphi\land\chi)\in s\text{ for all }\chi\}$;

• •

$V^{c}(p)=\{s\in S^{c}\mid p\in s\}$.

As mentioned, the semantics of $\Delta$ is a special case of the semantics of $\boxplus$ when $R_{1}=R_{2}$. In that case, we should have $R^{c}_{1}=R^{c}_{2}$. Indeed this is true, since in that case, $\boxplus\varphi\leftrightarrow\boxplus\neg\varphi$ is valid, and then the definition of $R_{2}^{c}$ is equivalent to that “$\text{for all }\varphi,\text{ if }\boxplus(\varphi\vee\psi)\in s\text{ for all }\psi,\text{ then }\varphi\in t$”, that is, the definition of $R^{c}_{1}$. And in this way, we obtain the canonical relation defined in [Kuh95] as a special case.

Let us look at the properties of the two functions $\lambda_{1}$ and $\lambda_{2}$.

Proposition 19**.**

Let $s\in S^{c}$. Then

1. (a)

$\lambda_{1}(s)\cap\lambda_{2}(s)$ is nonempty. Consequently, $\lambda_{1}(s)$ and $\lambda_{2}(s)$ are both nonempty. 2. (b)

$\lambda_{1}(s)$ and $\lambda_{2}(s)$ are both closed under conjunction. That is, if $\varphi_{1},\varphi_{2}\in\lambda_{1}(s)$, then $\varphi_{1}\land\varphi_{2}\in\lambda_{1}(s)$, and similarly for $\lambda_{2}(s)$. Consequently, $\lambda_{1}(s)$ and $\lambda_{2}(s)$ are both closed under finite conjunctions. 3. (c)

If $\varphi\in\lambda_{1}(s)$ and $\vdash\varphi\to\delta$, then $\delta\in\lambda_{1}(s)$, and similarly for $\lambda_{2}(s)$. 4. (d)

$\boxplus\varphi\in s$ iff either $\varphi\in\lambda_{1}(s)$ or $\neg\varphi\in\lambda_{2}(s)$.

Proof.

1. (a)

Since $\vdash\top$, then applying the rule $\text{RN}\boxplus$, we have $\vdash\boxplus\top\land\boxplus\neg\top$. By $\text{RE}\boxplus$, $\boxplus(\top\vee\psi)\in s$ for all $\psi$ and $\boxplus(\neg\top\land\chi)\in s$ for all $\chi$. Therefore, $\top\in\lambda_{1}(s)\cap\lambda_{2}(s)$. 2. (b)

Suppose that $\varphi_{1},\varphi_{2}\in\lambda_{1}(s)$, then $\boxplus(\varphi_{1}\vee\psi)\in s$ and $\boxplus(\varphi_{2}\vee\psi)\in s$ for all $\psi$. Then $\boxplus(\varphi_{1}\vee\psi)\land\boxplus(\varphi_{2}\vee\psi)\in s$. Using the axiom $\text{CON}\boxplus$, we obtain $\boxplus((\varphi_{1}\vee\psi)\land(\varphi_{2}\vee\psi))\in s$. Then applying the rule $\text{RE}\boxplus$, we infer that $\boxplus((\varphi_{1}\land\varphi_{2})\vee\psi)\in s$. Since $\psi$ is arbitrary, we now conclude that $\varphi_{1}\land\varphi_{2}\in\lambda_{1}(s)$.

Assume that $\varphi_{1},\varphi_{2}\in\lambda_{2}(s)$, then $\boxplus(\neg\varphi_{1}\land\chi)\in s$ and $\boxplus(\neg\varphi_{2}\land\chi)\in s$ for all $\chi$. Then $\boxplus(\neg\varphi_{1}\land\chi)\land\boxplus(\neg\varphi_{2}\land\chi)\in s$. Using the axiom $\text{CON}\boxplus$, we infer $\boxplus((\neg\varphi_{1}\land\chi)\vee(\neg\varphi_{2}\land\chi))\in s$. Now applying the rule $\text{RE}\boxplus$, we obtain $\boxplus((\neg(\varphi_{1}\land\varphi_{2})\land\chi))\in s$. Since $\chi$ is arbitrary, we now conclude that $\varphi_{1}\land\varphi_{2}\in\lambda_{2}(s)$. 3. (c)

Suppose $\varphi\in\lambda_{1}(s)$ and $\vdash\varphi\to\delta$, to show $\delta\in\lambda_{1}(s)$. By supposition, it follows that $\vdash\varphi\vee\delta\leftrightarrow\delta$ and $\boxplus(\varphi\vee\psi)\in s$ for all $\psi$. Then $\vdash\varphi\vee(\delta\vee\psi)\leftrightarrow\delta\vee\psi$. Applying the rule $\text{RE}\boxplus$, we derive $\vdash\boxplus(\varphi\vee(\delta\vee\psi))\leftrightarrow\boxplus(\delta\vee\psi)$. Since $\boxplus(\varphi\vee(\delta\vee\psi))\in s$, we derive that $\boxplus(\delta\vee\psi)\in s$. Since $\psi$ is arbitrary, $\delta\in\lambda_{1}(s)$.

Now assume that $\varphi\in\lambda_{2}(s)$ and $\vdash\varphi\to\delta$, to show $\delta\in\lambda_{2}(s)$. Since $\varphi\in\lambda_{2}(s)$, it follows that $\boxplus(\neg\varphi\land\chi)\in s$ for all $\chi$. Since $\vdash\varphi\to\delta$, it follows that $\vdash\neg\varphi\land\neg\delta\leftrightarrow\neg\delta$, and thus $\vdash\neg\varphi\land(\neg\delta\land\chi)\leftrightarrow\neg\delta\land\chi$. Applying the rule $\text{RE}\boxplus$, we obtain $\vdash\boxplus(\neg\varphi\land(\neg\delta\land\chi))\leftrightarrow\boxplus(\neg\delta\land\chi)$. Since $\boxplus(\neg\varphi\land(\neg\delta\land\chi))\in s$, we get $\boxplus(\neg\delta\land\chi)\in s$. Since $\chi$ is arbitrary, $\delta\in\lambda_{2}(s)$. 4. (d)

Suppose by contraposition that $\varphi\notin\lambda_{1}(s)$ and $\neg\varphi\notin\lambda_{2}(s)$. Then $\boxplus(\varphi\vee\psi)\notin s$ for some $\psi$, and $\boxplus(\neg\neg\varphi\land\chi)\notin s$ for some $\chi$, namely $\boxplus(\varphi\land\chi)\notin s$. Using the axiom $\text{DIS}\boxplus$, we obtain immediately $\boxplus\varphi\notin s$.

Conversely, assume that either $\varphi\in\lambda_{1}(s)$ or $\neg\varphi\in\lambda_{2}(s)$. Then either $\boxplus(\varphi\vee\psi)\in s$ for all $\psi$ or $\boxplus(\varphi\land\chi)\in s$ for all $\chi$. Then either case implies that $\boxplus\varphi\in s$: in the first case, letting $\psi=\bot$, by RE$\boxplus$ we obtain $\boxplus\varphi\in s$; in the second case, let $\chi=\top$, by RE$\boxplus$ again, we infer that $\boxplus\varphi\in s$. Therefore, $\boxplus\varphi\in s$.

∎

With the above results in preparation, we can obtain the following truth lemma.

Lemma 20**.**

For all $s\in S^{c}$, for all $\varphi\in\mathcal{L}(\boxplus)$, we have

[TABLE]

Proof.

By induction on $\varphi$. The only nontrivial case is $\boxplus\varphi$.

Assume for reductio that $\boxplus\varphi\in s$ but $\mathcal{M}^{c},s\nvDash\boxplus\varphi$. By induction hypothesis, there is a $t$ such that $sR_{1}^{c}t$ and $\varphi\notin t$, and there is a $u$ such that $sR_{2}^{c}u$ and $\neg\varphi\notin u$. Then by definitions of $R^{c}_{1}$ and $R^{c}_{2}$, we can obtain that $\varphi\notin\lambda_{1}(s)$ and $\neg\varphi\notin\lambda_{2}(s)$. This contradicts the supposition that $\boxplus\varphi\in s$ and Prop. 19(d).

Conversely, suppose $\boxplus\varphi\notin s$, we need to find two states $t$ and $u$ in $S^{c}$ such that $sR^{c}_{1}t$ and $\varphi\notin t$, and $sR^{c}_{2}u$ and $\varphi\in u$. For this, we first show that

1. (1)

$\lambda_{1}(s)\cup\{\neg\varphi\}$ is consistent, and 2. (2)

$\lambda_{2}(s)\cup\{\varphi\}$ is consistent.

If (1) does not hold, then there exist $\chi_{1},\cdots,\chi_{n}\in\lambda_{1}(s)$222Prop. 19(a) provides the nonempty of $\lambda_{1}(s)$. such that $\vdash\chi_{1}\land\cdots\land\chi_{n}\to\varphi$. Since $\chi_{1},\cdots,\chi_{n}\in\lambda_{1}(s)$, from Prop. 19(b) it follows that $\chi_{1}\land\cdots\land\chi_{n}\in\lambda_{1}(s)$. Then due to Prop. 19(c), we have $\varphi\in\lambda_{1}(s)$, by Prop. 19(d) we conclude that $\boxplus\varphi\in s$, contrary to the supposition.

If (2) does not hold, then there are $\psi_{1},\cdots,\psi_{m}\in\lambda_{2}(s)$333Again, Prop. 19(a) provides the nonempty of $\lambda_{2}(s)$. such that $\vdash\psi_{1}\land\cdots\land\psi_{m}\to\neg\varphi$. Since $\psi_{1},\cdots,\psi_{m}\in\lambda_{2}(s)$, it follows that $\psi_{1}\land\cdots\land\psi_{m}\in\lambda_{2}(s)$ from Prop. 19(b). Then thanks to Prop. 19(c), we infer that $\neg\varphi\in\lambda_{2}(s)$, by Prop. 19(d) again, we derive that $\boxplus\varphi\in s$, which contradicts the supposition again.

Then by Lindenbaum’s Lemma, we are done. ∎

Now it is a standard exercise to show that ${\bf K^{\boxplus}}$ is the minimal logic of $\mathcal{L}(\boxplus)$.

Theorem 21**.**

${\bf K^{\boxplus}}$ is sound and strongly complete with respect to the class of all bimodal frames.

6.3 The serial logic

In this section, we show that ${\bf K^{\boxplus}}$ is also the serial logic of $\mathcal{L}(\boxplus)$, that is to say, ${\bf K^{\boxplus}}$ is sound and strongly complete with respect to the class of serial bimodal frames. For this, if $R^{c}_{1}$ and $R^{c}_{2}$ in Def. 18 are serial, then we are done. We first have the following key observation.

Proposition 22**.**

Define $\mathcal{M}^{c}$ as in Def. 18 and $s\in S^{c}$. Then the following conditions are equivalent:

$R^{c}_{1}(s)\neq\emptyset$. 2. 2.

$\bot\notin\lambda_{1}(s)$. 3. 3.

$\boxplus\psi\notin s$ for some $\psi$. 4. 4.

$\bot\notin\lambda_{2}(s)$. 5. 5.

$R^{c}_{2}(s)\neq\emptyset$.

Proof.

We show $\ref{prop.serial-1}\Longleftrightarrow\ref{prop.serial-2}$, $\ref{prop.serial-2}\Longleftrightarrow\ref{prop.serial-3}$, $\ref{prop.serial-3}\Longleftrightarrow\ref{prop.serial-4}$, and $\ref{prop.serial-4}\Longleftrightarrow\ref{prop.serial-5}$. ∎

Proof.

$\ref{prop.serial-1}\Longleftrightarrow\ref{prop.serial-2}$: suppose towards contradiction that $R^{c}_{1}(s)\neq\emptyset$ but $\bot\in\lambda_{1}(s)$. Then $sR^{c}_{1}t$ for some $t\in S^{c}$, that is, $\lambda_{1}(s)\subseteq t$, and therefore $\bot\in t$: a contradiction. Conversely, assume that $\bot\notin\lambda_{1}(s)$, we need to show that $s$ has a $R^{c}_{1}$-successor. It suffices to show that $\lambda_{1}(s)$ is consistent. If not, there exists $\varphi_{1},\cdots,\varphi_{n}\in\lambda_{1}(s)$ such that $\vdash\varphi_{1}\land\cdots\land\varphi_{n}\to\bot$. Using items (b) and (c) of Prop. 19, we can derive that $\bot\in\lambda_{1}(s)$, which is contrary to the assumption.

$\ref{prop.serial-2}\Longleftrightarrow\ref{prop.serial-3}$: Suppose by contraposition that $\boxplus\psi\in s$ for all $\psi$. Since $\vdash\psi\leftrightarrow\bot\vee\psi$, by RE$\boxplus$, it follows that $\vdash\boxplus\psi\leftrightarrow\boxplus(\bot\vee\psi)$, and then $\boxplus(\bot\vee\psi)\in s$, and therefore $\bot\in\lambda_{1}(s)$. Conversely, assume that $\bot\in\lambda_{1}(s)$, then $\boxplus(\bot\vee\psi)\in s$ for all $\psi$, and thus $\boxplus\psi\in s$ for all $\psi$.

$\ref{prop.serial-3}\Longleftrightarrow\ref{prop.serial-4}$: similar to the proof of $\ref{prop.serial-2}\Longleftrightarrow\ref{prop.serial-3}$.

$\ref{prop.serial-4}\Longleftrightarrow\ref{prop.serial-5}$: similar to the proof of $\ref{prop.serial-1}\Longleftrightarrow\ref{prop.serial-2}$. ∎

Corollary 23**.**

Define $\mathcal{M}^{c}$ as in Def. 18. Then the following conditions are equivalent:

$R^{c}_{1}$ is serial. 2. 2.

$\bot\notin\lambda_{1}(s)$ for any $s\in S^{c}$. 3. 3.

$\boxplus\psi\notin s$ for any $s\in S^{c}$ and for some $\psi$. 4. 4.

$\bot\notin\lambda_{2}(s)$ for any $s\in S^{c}$. 5. 5.

$R^{c}_{2}$ is serial.

As we cannot exclude the possibility that $\boxplus\psi\in s$ for some $s\in S$ and for all $\psi$, by the above result, we cannot provide that $R^{c}_{1}$ and $R^{c}_{2}$ are serial. We call such states $s$ ‘endpoints’. By Prop. 22, $s$ has neither $R^{c}_{1}$-successors nor $R^{c}_{2}$-successors.

We handle these endpoints by using a similar strategy of ‘reflexivizing the arrows in the canonical model’ used for showing the completeness of serial contingency logic in [Hum95, FWvD15]. In detail, define $\mathcal{M}^{\bf D}=\langle S^{c},R^{\bf D}_{1},R^{\bf D}_{2},V^{c}\rangle$ as $\mathcal{M}^{c}$ in Def. 18, except that $R^{\bf D}_{i}=R^{c}_{i}\cup\{(s,s)\mid s\text{ is an endpoint}\}$. It should be obvious that $\mathcal{M}^{\bf D}$ is serial. Moreover, the truth values of $\mathcal{L}(\boxplus)$-formulas are invariant under the model transformation: for all $s\in S^{c}$, by Prop. 22, $R^{c}_{1}(s)\neq\emptyset$ iff $R^{c}_{2}(s)\neq\emptyset$. If $s$ is an endpoint, then as $R^{c}_{1}(s)=R^{c}_{2}(s)=\emptyset$, it holds vacuously that $\mathcal{M}^{c},s\vDash\boxplus\varphi$; since $s\vDash\varphi$ or $s\vDash\neg\varphi$ and $R_{1}^{\bf D}(s)=R_{2}^{\bf D}(s)=\{s\}$, we have also that $\mathcal{M}^{\bf D},s\vDash\boxplus\varphi$. If $s$ has both $R^{c}_{1}$- and $R^{c}_{2}$-successors, then it is clear that $\mathcal{M}^{c},s\vDash\boxplus\varphi$ iff $\mathcal{M}^{\bf D},s\vDash\boxplus\varphi$, as desired. Consequently,

Theorem 24**.**

${\bf K^{\boxplus}}$ is sound and strongly complete with respect to the class of serial bimodal frames.

7 Axiomatizations for $\mathcal{L}(\boxdot)$

This section first provides the minimal logic for $\mathcal{L}(\boxdot)$ and shows its soundness and completeness, then explores its extensions over special frames.

7.1 Minimal logic

Definition 25**.**

The minimal logic of $\mathcal{L}(\boxdot)$, denoted ${\bf K^{\boxdot}}$, consists of the following axioms and inference rules:

[TABLE]

The proposition below will be used in Prop. 29.

Proposition 26**.**

The rule $\dfrac{\varphi\to\psi}{\boxdot\varphi\land\boxdot(\psi\to\varphi)\to\boxdot\psi}$, denoted $\text{wM}\boxdot$, is derivable in ${\bf K^{\boxdot}}$.

Proof.

Suppose that $\vdash\varphi\to\psi$, then $\vdash\varphi\leftrightarrow(\varphi\land\psi)$. By $\text{RE}\boxdot$, we have $\vdash\boxdot\varphi\leftrightarrow\boxdot(\varphi\land\psi)$. By axiom $\boxdot\text{CON}$, $\vdash\boxdot(\varphi\to\neg\psi)\land\boxdot(\neg\varphi\to\neg\psi)\to\boxdot((\varphi\to\neg\psi)\land(\neg\varphi\to\neg\psi))$. Since $\vdash(\varphi\to\neg\psi)\land(\neg\varphi\to\neg\psi)\leftrightarrow\neg\psi$, by $\text{RE}\boxdot$ it follows that $\vdash\boxdot((\varphi\to\neg\psi)\land(\neg\varphi\to\neg\psi))\leftrightarrow\boxdot\neg\psi$. Using PC, $\boxdot\text{EQU}$ and $\text{RE}\boxdot$, we obtain $\vdash\boxdot(\varphi\land\psi)\leftrightarrow\boxdot(\varphi\to\neg\psi)$ and $\vdash\boxdot(\psi\to\varphi)\leftrightarrow\boxdot(\neg\varphi\to\neg\psi)$ and $\vdash\boxdot\neg\psi\leftrightarrow\boxdot\psi$, and therefore $\vdash\boxdot\varphi\land\boxdot(\psi\to\varphi)\to\boxdot\psi$. ∎

Proposition 27**.**

${\bf K^{\boxdot}}$ is sound with respect to the class of all bimodal frames.

Proof.

We only show the validity of axioms $\boxdot\text{CON}$ and $\boxdot\text{DIS}$. Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ be an arbitrary bimodal model and $s\in S$.

For the validity of $\boxdot\text{CON}$, suppose that $\mathcal{M},s\vDash\boxdot\varphi\land\boxdot\psi$, then for all $t,u$ such that $sR_{1}t$ and $sR_{2}u$, we have that ($t\vDash\varphi$ iff $u\vDash\varphi$), and also that ($t\vDash\psi$ iff $u\vDash\psi$), thus $t\vDash\varphi\land\psi$ iff ($t\vDash\varphi$ and $t\vDash\psi$) iff ($u\vDash\varphi$ and $u\vDash\psi$) iff $u\vDash\varphi\land\psi$, and thus $s\vDash\boxdot(\varphi\land\psi)$.

For the validity of $\boxdot\text{DIS}$, suppose that $\mathcal{M},s\vDash\boxdot\varphi$, then for all $t,u$ such that $sR_{1}t$ and $sR_{2}u$, we have that ($t\vDash\varphi$ iff $u\vDash\varphi$). If $\varphi$ is true at both $t$ and $u$, then so is $\varphi\vee\psi$; if $\varphi$ is false at both $t$ and $u$, then $\neg\varphi$ is true at both points, and so is $\neg\varphi\vee\chi$. Therefore, $\mathcal{M},s\vDash\boxdot(\varphi\vee\psi)\vee\boxdot(\neg\varphi\vee\chi)$, as desired. ∎

In the remainder of this subsection, we show the strong completeness of ${\bf K^{\boxdot}}$. The following canonical model is inspired by that of the minimal noncontingency logic in [FWvD15] and the similarity between $\boxdot$-axioms and $\Delta$-axioms.

Definition 28**.**

A tuple $\mathcal{M}^{c}=\{S^{c},R^{c}_{1},R^{c}_{2},V^{c}\}$ is the canonical model of ${\bf K^{\boxdot}}$, if

• •

$S^{c}=\{s\mid s\text{ is a maximal }{\bf K^{\boxdot}}\text{-consistent set}\}$,

• •

For $i\in\{1,2\}$, $sR^{c}_{i}t$ iff there exists $\chi$ such that

$\neg\boxdot\chi\in s$ and 2. 2.

for all $\varphi$, if $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$, then $\varphi\in t$.

• •

$V^{c}(p)=\{s\in S^{c}\mid p\in s\}$.

Note that $R^{c}_{1}=R^{c}_{2}$. This fact will make our proofs much more convenient.

Proposition 29**.**

Let $s\in S^{c}$, $\boxdot\varphi\notin s$ and $\Gamma(s)=\{\psi\mid\boxdot\psi\land\boxdot(\varphi\to\psi)\in s\}$. Then

$\Gamma(s)$ is nonempty. 2. 2.

If $\psi,\chi\in\Gamma(s)$, then $\psi\land\chi\in\Gamma(s)$. 3. 3.

If $\psi\in\Gamma(s)$, then $\nvdash\psi\to\varphi$. 4. 4.

$\Gamma(s)\cup\{\varphi\}$ and $\Gamma(s)\cup\{\neg\varphi\}$ are both consistent.

Proof.

Suppose that the preconditions hold. Then $\boxdot\neg\varphi\notin s$.

Straightforward because $\vdash\boxdot\top$. 2. 2.

Assume that $\psi,\chi\in\Gamma(s)$, then $\boxdot\psi\land\boxdot(\varphi\to\psi)\in s$ and $\boxdot\chi\land\boxdot(\varphi\to\chi)\in s$. By axiom $\boxdot\text{CON}$, it follows that $\boxdot(\psi\land\chi)\land\boxdot(\varphi\to\psi\land\chi)\in s$, and therefore $\psi\land\chi\in\Gamma(s)$. 3. 3.

Assume for reductio that $\psi\in\Gamma(s)$ and $\vdash\psi\to\varphi$. Then $\boxdot\psi\land\boxdot(\varphi\to\psi)\in s$ and $\vdash\boxdot\psi\land\boxdot(\varphi\to\psi)\to\boxdot\varphi$ (by the rule $\text{wM}\boxdot$ in Prop. 26), and therefore $\boxdot\varphi\in s$, which contradicts the supposition that $\boxdot\varphi\notin s$. 4. 4.

Assume that $\Gamma(s)\cup\{\varphi\}$ is inconsistent, then there exists $\psi_{1},\cdots,\psi_{m}\in\Gamma(s)$ (1 provides the nonempty of $\Gamma(s)$) such that $\vdash\psi_{1}\land\cdots\land\psi_{m}\to\neg\varphi$. By application of 2 for $m-1$ times, we can obtain that $\psi_{1}\land\cdots\land\psi_{m}\in\Gamma(s)$, which contradicts 3. Thus $\Gamma(s)\cup\{\varphi\}$ is consistent. Similarly, we can conclude that $\Gamma(s)\cup\{\neg\varphi\}$ is consistent.

∎

Lemma 30** (Truth Lemma for ${\bf K^{\boxdot}}$).**

For all $s\in S^{c}$, for all $\varphi\in\mathcal{L}(\boxdot)$, we have

[TABLE]

Proof.

By induction on $\varphi\in\mathcal{L}(\boxdot)$. The nontrivial case is $\boxdot\varphi$.

Suppose that $\boxdot\varphi\in s$ (thus $\boxdot\neg\varphi\in s$), to show that $\mathcal{M}^{c},s\vDash\boxdot\varphi$. If not, by induction hypothesis, there exist $t,u\in S^{c}$ such that $sR^{c}_{1}t$ and $sR^{c}_{2}u$ and it is not the case that ($\varphi\in t$ iff $\varphi\in u$). W.l.o.g. we may assume444This is because $R^{c}_{1}=R^{c}_{2}$. that $\varphi\in t$ but $\varphi\notin u$. From $sR^{c}_{1}t$, it follows that there exists $\chi$ such that $\neg\boxdot\chi\in s$ and (1) for all $\varphi$, if $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$, then $\varphi\in t$. Since $\neg\varphi\notin t$ and $\boxdot\neg\varphi\in s$, by (1) we have $\boxdot(\chi\to\neg\varphi)\notin s$, namely $\boxdot(\neg\varphi\vee\neg\chi)\notin s$. Similarly, from $sR^{c}_{2}u$ and $\varphi\notin u$, we can show that for some $\psi$, $\boxdot(\psi\to\varphi)\notin s$, that is, $\boxdot(\varphi\vee\neg\psi)\notin s$. Now by axiom $\boxdot\text{DIS}$, we obtain that $\boxdot\varphi\notin s$, which is contrary to the supposition.

Conversely, assume that $\boxdot\varphi\notin s$, we need to find two states $t,u\in S^{c}$ such that $sR^{c}_{1}t$ and $sR^{c}_{2}u$ and it is not the case that ($\varphi\in t$ iff $\varphi\in u$). Define $\Gamma(s)$ as in Prop. 29. By Prop. 29.4, $\Gamma(s)\cup\{\varphi\}$ and $\Gamma(s)\cup\{\neg\varphi\}$ are both consistent. Then by Lindenbaum’s Lemma, there are two states $t,u\in S^{c}$ such that $sR^{c}_{1}t$ and $sR^{c}_{2}u$ such that $\varphi\in t$ and $\varphi\notin u$, and thus it is not the case that ($\varphi\in t$ iff $\varphi\in u$), as desired. ∎

The strong completeness is now a standard exercise.

Theorem 31**.**

${\bf K^{\boxdot}}$ is sound and strongly complete with respect to the class of all bimodal frames.

7.2 Extensions

In this section, we study the axiomatizations of $\mathcal{L}(\boxdot)$ over special frames. The following table lists extra axioms and proof systems, and the frame properties that the corresponding systems characterize.

[TABLE]

In the above table, $qt,pt,qe,pe$ abbreviate quasi-transitivity, pseudo-transitivity, quasi-Euclidicity and pseudo-Euclidicity, respective, which are formalized by $\forall xyz(xR_{i}y\land yR_{j}z\to xR_{j}z)$, $\forall xyz(xR_{i}y\land yR_{j}z\to xR_{1}z\land xR_{2}z)$, $\forall xyz(xR_{i}y\land xR_{j}z\to yR_{j}z)$, and $\forall xyz(xR_{i}y\land xR_{j}z\to yR_{1}z\land yR_{2}z)$, respectively, where $i,j\in\{1,2\}$.

7.2.1 Serial logic

Thm. 31 shows that ${\bf K^{\boxdot}}$ is the minimal $\boxdot$-logic. We now demonstrate that the same system is also the serial $\boxdot$-logic, that is, ${\bf K^{\boxdot}}$ is also sound and strongly complete with respect to the class of serial bimodal frames. For this, we only need to show that $R^{c}_{1}$ and $R^{c}_{2}$ are both serial, which though cannot be guaranteed due to the possibility that all formulas of the form $\boxdot\varphi$ belongs to some state. Due to the fact that $R^{c}_{1}=R^{c}_{2}$, we call the points that have neither $R^{c}_{1}$- nor $R^{c}_{2}$-successors ‘$R^{c}$-dead points’.555Notice that as $R^{c}_{1}=R^{c}_{2}$, for all $s\in S^{c}$, $s$ either has both $R^{c}_{1}$- and $R^{c}_{2}$-successors, or has neither of them. We handle these points by using a similar strategy to the completeness proof of ${\bf K^{\boxplus}}$ over serial frames (see the remarks before Thm. 24). In detail, define $\mathcal{M}^{\bf D}=\langle S^{c},R^{\bf D}_{1},R^{\bf D}_{2},V^{c}\rangle$ as $\mathcal{M}^{c}$ in Def. 28, except that $R^{\bf D}_{i}=R^{c}_{i}\cup\{(s,s)\mid s\text{ is a }R^{c}\text{-dead points}\}$. It should be obvious that $\mathcal{M}^{\bf D}$ is serial. Moreover, the truth values of $\mathcal{L}(\boxdot)$-formulas are invariant under the model transformation: for all $s\in S^{c}$, if $s$ has both $R^{c}_{1}$- and $R^{c}_{2}$-successors, then it is clear that $\mathcal{M}^{c},s\vDash\boxdot\varphi$ iff $\mathcal{M}^{\bf D},s\vDash\boxdot\varphi$; if $s$ is a $R^{c}$-dead point, then $\mathcal{M}^{c},s\vDash\boxdot\varphi$ and $\mathcal{M}^{\bf D},s\vDash\boxdot\varphi$, as desired.

The above strategy indicates that $\mathcal{M}^{c}$ can be transformed into an equivalent serial bimodal model. In the sequel, we will show a stronger result: every bimodal model can be transformed into an equivalent serial bimodal model; more precisely, each bimodal model is a $\boxdot$-morphic image of some serial bimodal model.

Given a bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$, each world $s$ in $S$ has four possibilities: $s$ has neither $R_{1}$-successors nor $R_{2}$-successors, $s$ has $R_{1}$-successors but has no $R_{2}$-successors, $s$ has no $R_{1}$-successors but has $R_{2}$-successors, $s$ has both $R_{1}$-successors and $R_{2}$-successors. We handle this four different kinds of worlds in different ways, based on the following key observations.

$s$ has neither $R_{1}$-successors nor $R_{2}$-successors. In this case, we just add the $R_{1}$ and $R_{2}$ arrows from $s$ to itself. 2. 2.

$s$ has $R_{1}$-successors but has no $R_{2}$-successors. In this case, we first replace $s$ with some of its new copies, such that each copy has only one $R_{1}$-successor, then add the $R_{2}$-arrow from each copy to its sole $R_{1}$-successor. 3. 3.

$s$ has no $R_{1}$-successors but has $R_{2}$-successors. The method for dealing with this case is similar to that for the second case. We first replace $s$ with some of its new copies, such that each copy has only one $R_{2}$-successor, then add the $R_{1}$-arrow from each copy to its sole $R_{2}$-successor. 4. 4.

$s$ has both $R_{1}$-successors (say $t$) and $R_{2}$-successors (say $u$). In this case, if for instance, $t$ lies in the first case or the current case, we just keep the point $t$ and the arrow from $s$ to $t$. However, if $t$ lies in other two cases, then we cannot simply do the same thing (otherwise the truth values of formulas may change during the tranformation); instead, we need to replace $t$ with some of its new copies and deal with $t$ in the same way as in the second and third cases.

Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$. Define $E_{1}=\{s\in S\mid sR_{1}t\text{ for some }t\in S\}$ and $E_{2}=\{s\in S\mid sR_{2}t\text{ for some }t\in S\}$, and let $\overline{E_{1}}=S\backslash E_{1}$ and $\overline{E_{2}}=S\backslash E_{2}$.

It is not hard to see that $S$ can be partitioned into four areas: $\overline{E_{1}}\cap\overline{E_{2}}$, $E_{1}\cap\overline{E_{2}}$, $\overline{E_{1}}\cap E_{2}$ and $E_{1}\cap E_{2}$.

Definition 32**.**

Given any bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$, we construct a bimodal model $\mathcal{M}^{\prime}=\langle S^{\prime},R^{\prime}_{1},R^{\prime}_{2},V^{\prime}\rangle$, where

• •

$S^{\prime}=(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})\cup\{(s,t,1)\mid s\in E_{1}\cap\overline{E_{2}},sR_{1}t\}\cup\{(s,t,2)\mid s\in\overline{E_{1}}\cap E_{2},sR_{2}t\}$

• •

$sR^{\prime}_{1}t$ iff one of the following conditions holds:

$s\in\overline{E_{1}}\cap\overline{E_{2}}$ and $s=t$ 2. 2.

$s\in E_{1}\cap E_{2}$ and $sR_{1}t$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$ 3. 3.

$s\in E_{1}\cap E_{2}$ and $t=(t^{\prime},u,i)\in S^{\prime}$ and $sR_{1}t^{\prime}$, where $i\in\{1,2\}$ 4. 4.

$s=(s^{\prime},t,i)\in S^{\prime}$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$, where $i\in\{1,2\}$ 5. 5.

$s=(s^{\prime},t^{\prime},i)\in S^{\prime}$ and $t=(t^{\prime},u^{\prime},j)\in S^{\prime}$, where $i,j\in\{1,2\}$

• •

$sR^{\prime}_{2}t$ iff one of the following holds:

$s\in\overline{E_{1}}\cap\overline{E_{2}}$ and $s=t$ 2. 2.

$s\in E_{1}\cap E_{2}$ and $sR_{2}t$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$ 3. 3.

$s\in E_{1}\cap E_{2}$ and $t=(t^{\prime},u,i)\in S^{\prime}$ and $sR_{2}t^{\prime}$, where $i\in\{1,2\}$ 4. 4.

$s=(s^{\prime\prime},t,i)\in S^{\prime}$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$, where $i\in\{1,2\}$ 5. 5.

$s=(s^{\prime\prime},t^{\prime\prime},i)\in S^{\prime}$ and $t=(t^{\prime\prime},u^{\prime\prime},j)\in S^{\prime}$, where $i,j\in\{1,2\}$

• •

$V^{\prime}(p)=\{s\in S^{\prime}\mid g(s)\in V(p)\}$, where $g$ is a function from $S^{\prime}$ to $S$ such that $g(s)=s$ for $s\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$, and $g((s,t,i))=s$ for $(s,t,i)\in S^{\prime}$ where $i\in\{1,2\}$.

It would be constructive to give a concrete example. We choose the following example to cover all conditions in the definitions of the relations $R_{1}^{\prime}$ and $R_{2}^{\prime}$ (for the sake of simplicity, we leave out the valuations).

Example 33**.**

[TABLE]

In the left-hand model $\mathcal{M}$, it is not hard to see that $s\in E_{1}\cap E_{2}$, $u\in\overline{E_{1}}\cap E_{2}$, $v\in E_{1}\cap\overline{E_{2}}$, and $t,w\in\overline{E_{1}}\cap\overline{E_{2}}$. Thus in the right-hand model $\mathcal{M}^{\prime}$, $s,t,w$ are kept unchanged, whereas $u$ and $v$ are replaced by their new copies $(u,v,2)$ (since $uR_{2}v$), $(v,w,1)$ (since $vR_{1}w$), respectively.

Now for the arrows in $\mathcal{M}^{\prime}$, viz. accessibility relations. The $1$- and $2$-arrows from $t$ to itself and from $w$ to itself are obtained from the first conditions of (the definitions of) $R_{1}^{\prime}$ and $R_{2}^{\prime}$. The $1$- and $2$-arrows from $s$ to $t$ follow from the second conditions of $R_{1}^{\prime}$ and $R_{2}^{\prime}$. The $1$-arrow from $s$ to $(u,v,2)$ is derived from the third condition of $R_{1}^{\prime}$. The $2$-arrow from $s$ to $(v,w,1)$ is deduced from the third condition of $R_{2}^{\prime}$. The $1$- and $2$-arrows from $(v,w,1)$ to $w$ are inferred due to the fourth conditions of $R_{1}^{\prime}$ and $R_{2}^{\prime}$. The $1$- and $2$-arrows from $(u,v,2)$ to $(v,w,1)$ are concluded by the fifth conditions of $R_{1}^{\prime}$ and $R_{2}^{\prime}$. In this way, we transform the non-serial model $\mathcal{M}$ into the desired serial model $\mathcal{M}^{\prime}$.

The following proposition states that $\mathcal{M}^{\prime}$ constructed via Def. 32 is indeed serial.

Proposition 34**.**

$\mathcal{M}^{\prime}$ is serial.

Proof.

Let $s\in S^{\prime}$ be arbitrary. We need to show that there are $x,y\in S^{\prime}$ such that $sR^{\prime}_{1}x$ and $sR^{\prime}_{2}y$.

According to the definition of $S^{\prime}$, we distinguish the following cases.

$s\in\overline{E_{1}}\cap\overline{E_{2}}$. Then by the first conditions of the definitions of $R_{1}^{\prime}$ and $R^{\prime}_{2}$, $s$ is the desired $x$ and $y$. 2. 2.

$s\in E_{1}\cap E_{2}$. Then $sR_{1}t$ for some $t\in S$. We consider all possibilities of $t$ as follows.

1. (a)

$t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$. According to the second condition of the definition of $R^{\prime}_{1}$, we have $sR^{\prime}_{1}t$, and thus $t$ is the desired $x$. 2. (b)

$t\in(E_{1}\cap\overline{E_{2}})\cup(\overline{E_{1}}\cap E_{2})$. Then $tR_{i}u$ for some $u\in S^{c}$, where the value of $i$ depends on $t$: if $t\in E_{1}\cap\overline{E_{2}}$, then $i=1$; otherwise $i=2$. Then $(t,u,i)\in S^{\prime}$. According to the third condition of the definition of $R^{\prime}_{1}$, we infer $sR^{\prime}_{1}(t,u,i)$, thus $(t,u,i)$ is the desired $x$.

We have also $sR_{2}u$ for some $u\in S$. With a similar argument, we can obtain $sR^{\prime}_{2}y$ for some $y\in S^{\prime}$. 3. 3.

$s=(s^{\prime},t,i)\in S^{\prime}$ where $i\in\{1,2\}$. Then $s^{\prime}\in E_{i}\cap\overline{E_{j}}$ and $s^{\prime}R_{i}t$, where $j\in\{1,2\}$ and $j\neq i$. Again, since $t\in S$, we consider all possibilities of $t$ as follows.

1. (a)

$t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$. According to the fourth conditions of the definitions of $R^{\prime}_{1}$ and $R^{\prime}_{2}$, we get $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}t$, and thus $t$ is the desired $x$ and $y$. 2. (b)

$t\in(E_{1}\cap\overline{E_{2}})\cup(\overline{E_{1}}\cap E_{2})$. Then $tR_{k}u$ for some $u\in S$, where the value of $k$ depends on $t$: if $t\in E_{1}\cap\overline{E_{2}}$, then $k=1$; otherwise $k=2$. Then $(t,u,k)\in S^{\prime}$. According to the fifth conditions of the definitions of $R^{\prime}_{1}$ and $R^{\prime}_{2}$, we have $sR^{\prime}_{1}(t,u,k)$ and also $sR^{\prime}_{2}(t,u,k)$, and thus $(t,u,k)$ is the desired $x$ and $y$.

We have thus shown that in all cases, there always exist $x,y\in S^{\prime}$ such that $sR^{\prime}_{1}x$ and $sR^{\prime}_{2}y$, as desired. ∎

The proposition below indicates that $g$ satisfies the condition (Forth) of a $\boxdot$-morphism.

Proposition 35**.**

If $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}u$ and $g(t)\neq g(u)$, then $g(s)R_{1}g(t)$ and $g(s)R_{2}g(u)$.

Proof.

Suppose that $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}u$ and $g(t)\neq g(u)$, thus $t\neq u$. Since $s\in S^{\prime}$, we consider the following cases.

$s\in\overline{E_{1}}\cap\overline{E_{2}}$. According to the first condition of the definition of $R^{\prime}_{1}$ and $R^{\prime}_{2}$, we would have $s=t$ and $s=u$, which implies that $t=u$. Contradiction. 2. 2.

$s\in E_{1}\cap E_{2}$. Then $g(s)=s$. Since $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}u$, according to the second and third conditions of the definitions of $R_{1}^{\prime}$ and $R^{\prime}_{2}$, we consider four subcases.

1. (a)

$sR_{1}t$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$ and $sR_{2}u$ and $u\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$. In this case, we have $g(t)=t$ and $g(u)=u$, and therefore $g(s)R_{1}g(t)$ and $g(s)R_{2}g(u)$. 2. (b)

$sR_{1}t$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$ and $u=(u^{\prime},y,i)\in S^{\prime}$ and $sR_{2}u^{\prime}$, where $i\in\{1,2\}$. In this case, $g(t)=t$ and $g(u)=u^{\prime}$, and therefore $g(s)R_{1}g(t)$ and $g(s)R_{2}g(u)$. 3. (c)

$t=(t^{\prime},x,i)\in S^{\prime}$ and $sR_{1}t^{\prime}$, where $i\in\{1,2\}$ and $sR_{2}u$ and $u\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$. In this case, $g(t)=t^{\prime}$ and $g(u)=u$, and then $g(s)R_{1}g(t)$ and $g(s)R_{2}g(u)$. 4. (d)

$t=(t^{\prime},x,i)\in S^{\prime}$ and $sR_{1}t^{\prime}$ and $u=(u^{\prime},y,j)\in S^{\prime}$ and $sR_{2}u^{\prime}$, where $i,j\in\{1,2\}$. In this case, we have $g(t)=t^{\prime}$ and $g(u)=u^{\prime}$, and therefore $g(s)R_{1}g(t)$ and $g(s)R_{2}g(u)$. 3. 3.

$s$ is of the form $(x,y,i)\in S^{\prime}$, where $i\in\{1,2\}$. Since $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}u$, according to the fourth and fifth conditions of the definitions of $R^{\prime}_{1}$ and $R^{\prime}_{2}$, we consider four subcases.

1. (a)

$s=(s^{\prime},t,i)\in S^{\prime}$ and $s=(s^{\prime\prime},u,j)\in S^{\prime}$ and $t,u\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$, where $i,j\in\{1,2\}$. In this case, we would have $t=u$: a contradiction. 2. (b)

$s=(s^{\prime},t,i)\in S^{\prime}$ and $t\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$ and $u=(t,y,j)\in S^{\prime}$, where $i,j\in\{1,2\}$. In this case, $t\in(E_{1}\cap\overline{E_{2}})\cup(\overline{E_{1}}\cap E_{2})$: a contradiction. 3. (c)

$s=(s^{\prime\prime},u,i)\in S^{\prime}$ and $u\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$ and $t=(u,x,j)\in S^{\prime}$, where $i,j\in\{1,2\}$. In this case, $u\in(E_{1}\cap\overline{E_{2}})\cup(\overline{E_{1}}\cap E_{2})$: a contradiction. 4. (d)

$s=(s^{\prime},t^{\prime},i)\in S^{\prime}$ and $t=(t^{\prime},x,j)\in S^{\prime}$ and $u=(t^{\prime},y,k)\in S^{\prime}$, where $i,j,k\in\{1,2\}$. In this case, we would have $g(t)=g(u)=t^{\prime}$: a contradiction.

∎

It is worth remarking that the precondition ‘$g(t)\neq g(u)$’ in the statement of the above proposition cannot be weakened to ‘$t\neq u$’. For instance, in $\mathcal{M}$, $s^{\prime}R_{1}t^{\prime}$ and $t^{\prime}R_{1}x$ and $t^{\prime}R_{1}y$ and $x\neq y$ but $s^{\prime}$ and $t^{\prime}$ both have no $R_{2}$-successors. According to the fifth conditions of our definitions of $R^{\prime}_{1}$ and $R^{\prime}_{2}$, in $\mathcal{M}^{\prime}$, $(s^{\prime},t^{\prime},1)R_{1}^{\prime}(t^{\prime},x,1)$ and $(s^{\prime},t^{\prime},1)R_{2}^{\prime}(t^{\prime},y,1)$ and $(t^{\prime},x,1)\neq(t^{\prime},y,1)$. However, $g(s^{\prime},t^{\prime},1)=s^{\prime}$, which implies that $g(s^{\prime},t^{\prime},1)$ has no $R_{2}$-successors, thus we have no $g(s^{\prime},t^{\prime},1)R_{2}g(t^{\prime},y,1)$.

The following result states that $g$ also satisfies the condition (Back) of a $\boxdot$-morphism.

Proposition 36**.**

If $g(s)R_{1}t^{\prime}$ and $g(s)R_{2}u^{\prime}$ and $t^{\prime}\neq u^{\prime}$, then there are $t$ and $u$ in $S^{\prime}$ such that $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}u$ and $g(t)=t^{\prime}$ and $g(u)=u^{\prime}$.

Proof.

We show a stronger result:

($\ast$)   If $g(s)R_{1}t^{\prime}$ and $g(s)R_{2}u^{\prime}$, then there are $t$ and $u$ in $S^{\prime}$ such that $sR^{\prime}_{1}t$ and $sR^{\prime}_{2}u$ and $g(t)=t^{\prime}$ and $g(u)=u^{\prime}$.

Assume that $g(s)R_{1}t^{\prime}$ and $g(s)R_{2}u^{\prime}$. It is easy to see that $g(s)\in E_{1}\cap E_{2}$. Then we must have $g(s)=s$: otherwise, by the definition of $g$, $g(s)=s^{\prime}$ and $s=(s^{\prime},x,i)\in S^{\prime}$ where $i\in\{1,2\}$, then $s^{\prime}\in E_{1}\cap E_{2}$ and either $s^{\prime}\in E_{1}\cap\overline{E_{2}}$ or $s^{\prime}\in\overline{E_{1}}\cap E_{2}$, which is impossible. Thus $sR_{1}t^{\prime}$ and $sR_{2}u^{\prime}$. Since $t^{\prime}\in S$, we have the following cases.

• •

$t^{\prime}\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$. Then by the second conditions of $R^{\prime}_{1}$, it follows that $sR^{\prime}_{1}t^{\prime}$; by the definition of $g$, $g(t^{\prime})=t^{\prime}$. Therefore, $t^{\prime}$ is the desired $t$.

• •

$t^{\prime}\in E_{i}\cap\overline{E_{j}}$, where $i,j\in\{1,2\}$ and $i\neq j$. In this case, $t^{\prime}R_{i}x$ for some $x$, then $(t^{\prime},x,i)\in S^{\prime}$. By the third condition of the definition of $R^{\prime}_{1}$, $sR^{\prime}_{1}(t^{\prime},x,i)$; by the definition of $g$, $g(t^{\prime},x,i)=t^{\prime}$. Therefore, $(t^{\prime},x,i)$ is the desired $t$.

We have thus shown that there exists $t\in S^{\prime}$ such that $sR^{\prime}_{1}t$ and $g(t)=t^{\prime}$.

Similarly, from $u^{\prime}\in S$ and $sR_{2}u^{\prime}$, we can show that there exists $u\in S^{\prime}$ such that $sR^{\prime}_{2}u$ and $g(u)=u^{\prime}$, as desired.

∎

We have now shown that $g$ is a $\boxdot$-morphism from $\mathcal{M}^{\prime}$ to $\mathcal{M}$. Then by Prop. 12, we immediately have

Lemma 37**.**

For all $s\in S^{\prime}$, for all $\varphi\in\mathcal{L}(\boxdot)$, we have

[TABLE]

To show the completeness, we also need the following result.

Lemma 38**.**

$g$ is surjective.

Proof.

Suppose that $s\in S$, to find a $x\in S^{\prime}$ such that $g(x)=s$. We consider two cases.

• •

$s\in(\overline{E_{1}}\cap\overline{E_{2}})\cup(E_{1}\cap E_{2})$. According to the definition of $g$, we have $g(s)=s$; clearly, $s\in S^{\prime}$.

• •

$s\in E_{i}\cap\overline{E_{j}}$, where $i,j\in\{1,2\}$ and $i\neq j$. Then $sR_{i}t$ for some $t$. It follows that $(s,t,i)\in S^{\prime}$. By the definition of $g$, we have $g(s,t,i)=s$.

∎

Theorem 39**.**

${\bf K^{\boxdot}}$ is sound and strongly complete with respect to the class of serial bimodal frames.

Proof.

Let $\Gamma$ be a consistent set. By Thm. 31, $\Gamma$ is satisfiable in a bimodal model, say $(\mathcal{M},s)$. We then construct $\mathcal{M}^{\prime}$ from $\mathcal{M}$ as in Def. 32. By Lemma 38, there exists $x\in S^{\prime}$ such that $g(x)=s$, and thus $\mathcal{M},g(x)\vDash\Gamma$. Then by Lemma 37, $\mathcal{M}^{\prime},x\vDash\Gamma$. We also know that $\mathcal{M}^{\prime}$ is serial by Prop. 34. Therefore, $\Gamma$ is satisfiable in a serial bimodal model, as desired. ∎

7.2.2 Reflexive logic

In this section, we show that ${\bf KT^{\boxdot}}$ is sound and strongly complete with respect to the class of reflexive bimodal frames. As we will see, ${\bf KT^{\boxdot}}$ is also sound and strongly complete with respect to the class of bimodal frames $\langle S,R_{1},R_{2}\rangle$ where either $R_{1}$ or $R_{2}$ is reflexive.

Proposition 40**.**

$\boxdot\text{T}$ is valid on the class of reflexive bimodal frames.

Proof.

Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ be an arbitrary reflexive bimodal model and $s\in S$. Suppose that $\mathcal{M},s\vDash\varphi\land\boxdot\varphi\land\boxdot(\varphi\to\psi)$, to show that $s\vDash\boxdot\psi$. Since $s\in R_{1}(s)\cap R_{2}(s)$, by Coro. 5, from $\mathcal{M},s\vDash\boxdot\varphi\land\boxdot(\varphi\to\psi)$ it follows that $s\vDash\Delta_{1}\varphi\land\Delta_{2}\varphi\land\Delta_{1}(\varphi\to\psi)\land\Delta_{2}(\varphi\to\psi)$. By the obtained result,666That is, $\varphi\land\Delta\varphi\land\Delta(\varphi\to\psi)\to\Delta\psi$ is valid over the class of reflexive frames $\langle S,R\rangle$, see e.g. [FWvD15]. we can show that $s\vDash\Delta_{1}\psi\land\Delta_{2}\psi$. Now using Coro. 5, we conclude that $\mathcal{M},s\vDash\boxdot\psi$. ∎

As one may easily verify, the above statement still holds if the class of reflexive bimodal frames is enlarged to the class of bimodal frames where at least one accessibility relation is reflexive, that is, $\boxdot\text{T}$ is valid over bimodal frames $\langle S,R_{1},R_{2}\rangle$ where $R_{1}$ or $R_{2}$ is reflexive.

Definition 41**.**

Define $\mathcal{M}^{c}$ w.r.t. ${\bf KT^{\boxdot}}$ as in Def. 28. We say $\mathcal{M}^{r}=\langle S^{c},R_{1}^{r},R^{r}_{2},V^{c}\rangle$ is the reflexive closure of $\mathcal{M}^{c}$, if for all $i\in\{1,2\}$, $R^{r}_{i}$ is the reflexive closure of $R^{c}_{i}$; in symbol, $R_{i}^{r}=R^{c}_{i}\cup\{(s,s)\mid s\in S\}$ for $i\in\{1,2\}$.

It is clear that $\mathcal{M}^{r}$ is a reflexive bimodal model.

Lemma 42** (Truth Lemma for ${\bf KT^{\boxdot}}$).**

For all $s\in S^{c}$, for all $\varphi\in\mathcal{L}(\boxdot)$, we have

[TABLE]

Proof.

By induction on $\varphi$. We only consider the nontrivial case $\boxdot\varphi$, that is to show, $\boxdot\varphi\in s$ iff $\mathcal{M}^{r},s\vDash\boxdot\varphi$.

‘If’: straightforward by Lemma 30 and the fact that $R^{c}_{i}\subseteq R^{r}_{i}$ for $i\in\{1,2\}$.

‘Only if’: Suppose, for a contradiction, that $\boxdot\varphi\in s$ but $\mathcal{M}^{r},s\nvDash\boxdot\varphi$. By induction hypothesis, there exist $t,u\in S^{c}$ such that $sR^{r}_{1}t$ and $sR^{r}_{2}u$ and $(\varphi\in t\not\Longleftrightarrow\varphi\in u)$. W.l.o.g. we may assume that $\varphi\in t$ but $\varphi\notin u$. If $s\neq t$ and $s\neq u$, then $sR^{c}_{1}t$ and $sR^{c}_{2}u$, and thus the proof continues as in the corresponding part in Lemma 30, and finally we can arrive at a contradiction. If $s=t$ or $s=u$, w.l.o.g. we assume that $s=t$, and thus $s\neq u$ (as $t\neq u$), hence $sR^{c}_{2}u$.

Since $s=t$ and $\varphi\in t$, we have $\varphi\in s$. Because $sR^{c}_{2}u$, there is a $\chi$ such that $\neg\boxdot\chi\in s$ and $({\dagger})$: for all $\psi$, if $\boxdot\psi\land\boxdot(\chi\to\psi)\in s$, then $\psi\in u$. By supposition $\boxdot\varphi\in s$ and the fact that $\varphi\notin u$, we derive that $\boxdot(\chi\to\varphi)\notin s$, that is, $\boxdot(\varphi\vee\neg\chi)\notin s$. Moreover, by axiom $\boxdot\text{T}$, $\vdash\varphi\to[\boxdot\varphi\to(\boxdot(\varphi\to\chi)\to\boxdot\chi)]$, then as $\varphi\land\boxdot\varphi\land\neg\boxdot\chi\in s$, $\boxdot(\neg\varphi\vee\chi)\notin s$. Now by axiom $\boxdot\text{DIS}$, it follows that $\boxdot\varphi\notin s$: a contradiction again. ∎

It is natural to ask if the above claim can be generalized to any bimodal model, that is, if every bimodal model has an equivalent reflexive closure. The answer is negative. For example, the following are a bimodal model and its reflexive closure, but one may check that $\mathcal{M},w\vDash\boxdot p$ whereas $\mathcal{M}^{r},w\nvDash\boxdot p$.

[TABLE]

With the soundness of ${\bf K^{\boxdot}}$ (Thm. ), Prop. 40 and its subsequent remark, Lindenbaum’s Lemma, and Lemma 42 in hand, the following result now follows straightforwardly.

Theorem 43**.**

${\bf KT^{\boxdot}}$ is sound and strongly complete with respect to the class of reflexive bimodal frames, and also with respect to the class of bimodal frames $\langle S,R_{1},R_{2}\rangle$ where either $R_{1}$ or $R_{2}$ is reflexive.

7.2.3 Symmetric logic

This part deals with the soundness and strong completeness of ${\bf KB^{\boxdot}}$ over the class of symmetric bimodal frames. For the soundness, it suffices to show the validity of $\boxdot\text{B}$. Recall that $\boxdot\text{B}$ denotes $\varphi\to\boxdot((\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi)$.

Proposition 44**.**

$\boxdot\text{B}$ is valid over the class of symmetric bimodal frames.

Proof.

Let $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ be a symmetric bimodal model and $s\in S$. Suppose, for a contradiction, that $\mathcal{M},s\vDash\varphi$ but $\mathcal{M},s\nvDash\boxdot((\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi)$. Then there exist $t,u$ such that $sR_{1}t$ and $sR_{2}u$ such that it is not the case that ($t\vDash(\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi$ iff $u\vDash(\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi$). W.l.o.g. we may assume that $u\nvDash(\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi$, i.e. $u\vDash(\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\land\neg\chi$.777The other case that $t\nvDash(\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)\to\chi$ can be shown similarly, by using the symmetry of $R_{1}$ instead.

By $u\vDash\neg\boxdot\psi$, there are $v,w$ such that $uR_{1}v$ and $uR_{2}w$ and ($v\vDash\psi\not\Longleftrightarrow w\vDash\psi$). Since $sR_{2}u$ and $R_{2}$ is symmetric, we have $uR_{2}s$. Since $s\vDash\varphi$ and $u\vDash\boxdot\varphi$ and $uR_{1}v$, it follows that $v\vDash\varphi$, and thus $w\vDash\varphi$. Together with ($v\vDash\psi\not\Longleftrightarrow w\vDash\psi$), this implies that $u\nvDash\boxdot(\varphi\to\psi)$: a contradiction. ∎

For the strong completeness, we adopt the following strategy: first show that ${\bf KB^{\boxdot}}$ is strongly complete with respect to the class of quasi-symmetric bimodal frames, then demonstrate that every quasi-symmetric bimodal model is a $\boxdot$-morphic image of some symmetric bimodal model.

We first note that $\varphi\to\boxdot(\boxdot\varphi\land\boxdot(\varphi\to\psi)\land\neg\boxdot\psi)$, denoted by $\text{w}\boxdot\text{B}$, is derivable in ${\bf KB^{\boxdot}}$.

Proposition 45**.**

Let $i\in\{1,2\}$ and $s,t\in S^{c}$ such that $\neg\boxdot\chi\in t$. If $sR_{i}^{c}t$, then $tR^{c}_{i}s$.

Proof.

Suppose, for a contradiction, that $\neg\boxdot\chi\in t$ and $sR_{i}^{c}t$ where $i\in\{1,2\}$ but it is not the case that $tR^{c}_{i}s$. Then from $sR_{i}^{c}t$, it follows that there exists $\psi$ such that $\neg\boxdot\psi\in s$ and $(\star)$: for all $\delta$, if $\boxdot\delta\land\boxdot(\psi\to\delta)\in s$, then $\delta\in t$. From $\neg\boxdot\chi\in t$ and $\sim tR^{c}_{i}s$, it follows that there exists $\varphi$ such that $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in t$ but $\varphi\notin s$ (that is, $\neg\varphi\in s$). By axiom $\boxdot\text{B}$, $\boxdot((\boxdot\neg\varphi\land\boxdot(\neg\varphi\to\neg\chi)\land\neg\boxdot\neg\chi)\to\neg\psi)\in s$; by $\text{w}\boxdot\text{B}$, $\boxdot(\boxdot\neg\varphi\land\boxdot(\neg\varphi\to\neg\chi)\land\neg\boxdot\neg\chi)\in s$. Using axioms $\boxdot\text{Equ}$ and PC and the rule $\text{RE}\boxdot$, we can show that $\boxdot\neg(\boxdot\varphi\land\boxdot(\chi\to\varphi)\land\neg\boxdot\chi)\in s$ and $\boxdot(\psi\to\neg(\boxdot\varphi\land\boxdot(\chi\to\varphi)\land\neg\boxdot\chi))\in s$. Then by $(\star)$, $\neg(\boxdot\varphi\land\boxdot(\chi\to\varphi)\land\neg\boxdot\chi))\in t$: a contradiction. ∎

Proposition 46**.**

Let $s\in S^{c}$. Then the following conditions are equivalent:

(1) $\neg\boxdot\chi\in s$ for some $\chi$;

(2) $sR^{c}_{1}t$ for some $t$;

(3) $sR^{c}_{2}u$ for some $u$.

Proof.

$(1)\Rightarrow(2)\&(3)$ can be obtained from item 4 of Prop. 29, whereas $(2)\Rightarrow(1)$ and $(3)\Rightarrow(1)$ follows from the definitions of $R^{c}_{1}$ and $R^{c}_{2}$. ∎

As a corollary of Prop. 45 and Prop. 46, we obtain the following result.

Corollary 47**.**

Let $i,j\in\{1,2\}$ and $s,t\in S^{c}$ such that $tR^{c}_{j}u$ for some $u\in S^{c}$. If $sR^{c}_{i}t$, then $tR^{c}_{i}s$.888In fact, we can get an alternative result: let $i,j\in\{1,2\}$ and $s,t\in S^{c}$ such that $\neg\boxdot\chi\in t$. If $sR_{i}^{c}t$, then $tR^{c}_{j}s$. This is due to the fact that $R^{c}_{1}=R^{c}_{2}$. But for our purpose of showing that every quasi-symmetric bimodal model is a $\boxdot$-morphic image of some symmetric bimodal model, we do not need the stronger correspondent (we say ‘stronger’ because in any quasi-symmetric bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$, we do not have $R_{1}=R_{2}$ in general).

Given a bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$, $\mathcal{M}$ is quasi-symmetric, if for $i,j\in\{1,2\}$, for all $s,t\in S$ with $tR_{j}u$ for some $u\in S$, $sR_{i}t$ implies $tR_{i}s$. Intuitively, for any point in a quasi-symmetric model, if it has a successor with respect to some index, then there is a converse arrow with respect to an index from that point to its predecessor (if any). With the notion in mind, it follows from Lemma 30 and Coro. 47 that

Theorem 48**.**

${\bf KB^{\boxdot}}$ is strongly complete with respect to the class of quasi-symmetric bimodal frames.

Given a quasi-symmetric bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$, to build a desired symmetric bimodal model, we need only handle those states in $\mathcal{M}$ that have either $R_{1}$-predecessors or $R_{2}$-predecessors but have neither $R_{1}$-successors nor $R_{2}$-successors. We collect as $T_{1}$ those states in $\mathcal{M}$ that have $R_{1}$-predecessors but have neither $R_{1}$-successors nor $R_{2}$-successors, and collect as $T_{2}$ those states in $\mathcal{M}$ that have $R_{2}$-predecessors but have neither $R_{1}$-successors nor $R_{2}$-successors. In symbol,

[TABLE]

[TABLE]

and we also define $\overline{T_{1}}=S\backslash T_{1}$ and $\overline{T_{2}}=S\backslash T_{2}$.

Definition 49**.**

Given any quasi-symmetric bimodal model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$, we define a bimodal model $\mathcal{M}^{+}=\langle S^{+},R^{+}_{1},R^{+}_{2},V^{+}\rangle$ in which

• •

$S^{+}=\overline{T_{1}}\cup\overline{T_{2}}\cup\{(s,t,1)\mid t\in T_{1}\text{ and }sR_{1}t\}\cup\{(s,t,2)\mid t\in T_{2}\text{ and }sR_{2}t\}$.

• •

$sR^{+}_{1}t$ iff one of the following conditions holds:

1. (i)

$t\in\overline{T_{1}}$ and $sR_{1}t$ 2. (ii)

$t=(s,t^{\prime},1)\in S^{+}$ 3. (iii)

$s=(t,s^{\prime},1)\in S^{+}$

• •

$sR^{+}_{2}t$ iff one of the following conditions holds:

1. (i)

$t\in\overline{T_{2}}$ and $sR_{2}t$ 2. (ii)

$t=(s,t^{\prime\prime},2)\in S^{+}$ 3. (iii)

$s=(t,s^{\prime\prime},2)\in S^{+}$

• •

$V^{+}(p)=\{s\in S^{+}\mid h(s)\in V(p)\}$, where $h$ is a function from $S^{+}$ to $S$ such that $h(s)=s$ for $s\in\overline{T_{1}}\cup\overline{T_{2}}$, and $h((s,t,i))=t$ for $(s,t,i)\in S^{+}$, where $i\in\{1,2\}$.

Note that $\mathcal{M}^{+}$ in [FWvD14, Def. 5.9] is a special case of $\mathcal{M}^{+}$ here when $R_{1}^{+}=R^{+}_{2}=R^{+}$, since $\mathcal{M}^{c}$ therein is an almost symmetric model and thus a quasi-symmetric model, and the condition that $p\in h(s)$ is equivalent to the condition that $h(s)\in V^{c}(p)$. Note that for instance, the condition (i) in the definition of $R^{+}_{1}$ is equivalent to the more complex one ‘$s,t\in\overline{T_{1}}$ and $sR_{1}t$’, since $sR_{1}t$ implies that $s\in\overline{T_{1}}$, and similarly for other conditions. An analogous simplification goes also to the cases (i)-(iii) in the definition $R^{+}$ in [FWvD14, Def. 5.9].999In detail, the definition of $R^{+}$ in [FWvD14, Def. 5.9] can be simplified into the following: $sR^{+}t$ iff one of the following cases holds: (i) $t\in\overline{D}$ and $sR^{c}t$, (ii) $t=(s,s^{\prime})\in S^{+}$, (iii) $s=(t,t^{\prime})\in S^{+}$.

Prop. 50—Prop. 52 together say that $h$ is a surjective $\boxdot$-morphism, and therefore $\mathcal{M}$ is a $\boxdot$-morphic image of $\mathcal{M}^{+}$.

Proposition 50**.**

[Forth] If $sR^{+}_{1}t$ and $sR^{+}_{2}u$ and $h(t)\neq h(u)$, then $h(s)R_{1}h(t)$ and $h(s)R_{2}h(u)$.

Proof.

We show a stronger result:

$(\ast)$   If $sR^{+}_{1}t$ and $sR^{+}_{2}u$ and $t\neq u$, then $h(s)R_{1}h(t)$ and $h(s)R_{2}h(u)$.

Suppose that $sR^{+}_{1}t$ and $sR^{+}_{2}u$ and $t\neq u$. Then the arrows from $s$ to $t$ and $u$ are both impossible to be constructed by the condition (iii), since otherwise $s=(t,s^{\prime},1)$ and $s=(u,s^{\prime\prime},2)$, which would entail that $t=u$, contradiction. In the sequel, it suffices to consider the remaining two conditions.

Since $sR^{+}_{1}t$, if $t\in\overline{T_{1}}$ and $sR_{1}t$, then obviously $s\in\overline{T_{1}}$, thus $h(s)=s$ and $h(t)=t$, and therefore $h(s)R_{1}h(t)$; if $t=(s,t^{\prime},1)\in S^{+}$, then $sR_{1}t^{\prime}$, obviously $s\in\overline{T_{1}}$, thus $h(s)=s$ and $h(t)=t^{\prime}$, and therefore $h(s)R_{1}h(t)$. Similarly, we can show $h(s)R_{2}h(u)$ by using $sR^{+}_{2}u$ instead. ∎

Proposition 51**.**

[Back] If $h(s)R_{1}t^{\prime}$ and $h(s)R_{2}u^{\prime}$ and $t^{\prime}\neq u^{\prime}$, then there exist $t,u\in S^{+}$ such that $sR_{1}^{+}t,sR_{2}^{+}u$ and $h(t)=t^{\prime}$ and $h(u)=u^{\prime}$.

Proof.

We show a stronger result:

$(\star)~{}~{}~{}$ For any $i\in\{1,2\}$, if $h(s)R_{i}t^{\prime}$, then there exist $t\in S^{+}$ such that $sR_{i}^{+}t$ and $h(t)=t^{\prime}$.

Let $i\in\{1,2\}$. Suppose that $h(s)R_{i}t^{\prime}$. It is clear that $h(s)\in\overline{T_{1}}\cap\overline{T_{2}}$. Then it must be that $h(s)=s$: otherwise, $h(s)=s^{\prime}$ for $s=(t,s^{\prime},j)\in S^{+}$, where $j\in\{1,2\}$, which would imply that $s^{\prime}\in\overline{T_{1}}\cap\overline{T_{2}}$ and $s^{\prime}\in T_{1}\cup T_{2}$, which is a contradiction. Hence $sR_{i}t^{\prime}$. Since $t^{\prime}\in S$, $t^{\prime}\in\overline{T_{i}}$ or $t^{\prime}\in T_{i}$. If $t^{\prime}\in\overline{T_{i}}$, then by the first condition of the definition of $R^{+}_{i}$, we infer $sR^{+}_{i}t^{\prime}$; by the definition of $h$, $h(t^{\prime})=t^{\prime}$. If $t^{\prime}\in T_{i}$, then $(s,t^{\prime},i)\in S^{+}$, and thus by the second condition of the definition of $R^{+}_{i}$, we derive $sR^{+}_{i}(s,t^{\prime},i)$; by the definition of $h$, we get $h((s,t^{\prime},i))=t^{\prime}$, as desired. ∎

Proposition 52**.**

The function $h$ is surjective.

Proof.

Suppose that $s\in S$, we need to find a $s^{\prime}\in S^{+}$ such that $h(s^{\prime})=s$.

If $s\in\overline{T_{1}}$, then $s\in S^{+}$ and $h(s)=s$; otherwise, $s\in T_{1}$, then there exists $x\in S$ such that $xR_{1}s$, thus $(x,s,1)\in S^{+}$, and then $h((x,s,1))=s$, as desired. ∎

Now using Prop. 12, we immediately have

Lemma 53**.**

For all $s\in S^{+}$, for all $\varphi\in\mathcal{L}(\boxdot)$, we have

[TABLE]

To finish the completeness of ${\bf KB^{\boxdot}}$, we need also show that $\mathcal{M}^{+}$ is symmetric.

Lemma 54**.**

$\mathcal{M}^{+}$ is symmetric.

Proof.

We need to show that $R_{1}^{+}$ and $R^{+}_{2}$ are both symmetric. We show only the symmetry of $R^{+}_{1}$, since the symmetry of $R^{+}_{2}$ can be proved analogously.

Suppose for any $s,t\in S^{+}$ we have $sR^{+}_{1}t$, to show that $tR^{+}_{1}s$. According to the definition of $R^{+}$, we consider three conditions.

• •

$t\in\overline{T_{1}}$ and $sR_{1}t$. Then $tR_{j}u$ for some $u\in S$, where $j\in\{1,2\}$. Since $\mathcal{M}$ is quasi-symmetric, we have $tR_{1}s$. Obviously, $s\in\overline{T_{1}}$. It then follows that $tR^{+}_{1}s$.

• •

$t=(s,t^{\prime},1)\in S^{+}$ for some $t^{\prime}$. By the third condition of the definition of $R^{+}_{1}$, it follows that $tR^{+}_{1}s$.

• •

$s=(t,s^{\prime},1)\in S^{+}$ for some $s^{\prime}$. By the second condition of the definition of $R^{+}_{1}$, it follows that $tR^{+}_{1}s$.

∎

Theorem 55**.**

${\bf KB^{\boxdot}}$ is strongly complete with respect to the class of symmetric bimodal frames.

Proof.

Let $\Sigma$ be a consistent set. By Thm. 48, $\Sigma$ is satisfiable in a quasi-symmetric bimodal model, say $(\mathcal{M},s)$. Construct $\mathcal{M}^{+}$ from $\mathcal{M}$ as in Def. 49. As $h$ is surjective (Prop. 52), there exists $x\in S^{+}$ such that $h(x)=s$, thus $\mathcal{M},h(x)\vDash\Sigma$. By Lemma 53 and Lemma 54, $\Sigma$ is satisfiable in a symmetric bimodal model $\mathcal{M}^{+}$, as required. ∎

7.2.4 Transitive-like and Euclidean-like logics

In contingency logic, $\Delta\varphi\to\Delta(\Delta\varphi\vee\psi)$ and $\neg\Delta\varphi\to\Delta(\neg\Delta\varphi\vee\psi)$, are added in the minimal contingency logic to axiomatize the class of transitive frames and the class of Euclidean frames, respectively, see e.g. [FWvD15]. It is then quite natural to expect that their $\boxdot$-counterparts $\boxdot\varphi\to\boxdot(\boxdot\varphi\vee\psi)$ (denoted $\boxdot 4$) and $\neg\boxdot\varphi\to\boxdot(\neg\boxdot\varphi\vee\psi)$, can be used to axiomatize this generalized logic over the same classes. Unfortunately, it turns out to be wrong, since $\boxdot 4$ and $\boxdot 5$ are not sound. In what follows, instead of showing this directly, we show that one of the weaker versions of each of them, viz. $\boxdot\varphi\to\boxdot\boxdot\varphi$ (denoted w$\boxdot 4$) and $\neg\boxdot\varphi\to\boxdot\neg\boxdot\varphi$ (denoted w$\boxdot 5$), are invalid over the corresponding frame class.

Proposition 56**.**

w$\boxdot 4$ is invalid over the class of transitive bimodal frames.

Proof.

Consider the following model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$:

[TABLE]

It can be checked easily that both $R_{1}$ and $R_{2}$ are transitive, and thus $\mathcal{M}$ is transitive. On one hand, since all $R_{1}$-successors $u$ and $R_{2}$-successors $t$ of $s$ agree on the truth value of $p$, we have $s\vDash\boxdot p$. On the other hand, because some $R_{1}$-successor $u$ and some $R_{2}$-successor $w$ of $u$ do not agree on the truth value of $p$, we obtain $u\nvDash\boxdot p$; since $t$ has no any successors, $t\vDash\boxdot p$, and thus $s\nvDash\boxdot\boxdot p$. Therefore, $s\nvDash\boxdot p\to\boxdot\boxdot p$. ∎

Proposition 57**.**

w$\boxdot 5$ is invalid over the class of Euclidean bimodal frames.

Proof.

Consider the following Euclidean model $\mathcal{M}^{\prime}=\langle S,R_{1},R_{2},V\rangle$:

[TABLE]

On one hand, $s\vDash\neg\boxdot p$: because $sR_{1}s$ and $sR_{2}t$ and $s\vDash p$ but $t\nvDash p$. On the other hand, $s\nvDash\boxdot\neg\boxdot p$: as $t$ has only a single successor, $t\vDash\boxdot p$, i.e. $t\nvDash\neg\boxdot p$, and thus $s\nvDash\boxdot\neg\boxdot p$. Therefore, $s\nvDash\neg\boxdot p\to\boxdot\neg\boxdot p$. ∎

Denote ${\bf K4^{\boxdot}}={\bf K^{\boxdot}}+\boxdot 4$ and ${\bf K5^{\boxdot}}={\bf K^{\boxdot}}+\boxdot 5$. As we have seen, ${\bf K4^{\boxdot}}$ and ${\bf K5^{\boxdot}}$ are not the transitive $\boxdot$-logic and Euclidean $\boxdot$-logic, respectively. It is then natural to ask which logics both proof systems are; in other words, which classes of frames are characterized by ${\bf K4^{\boxdot}}$ and ${\bf K5^{\boxdot}}$, respectively.

We remind the reader of the properties $qt$, $pt$, $qe$, $pe$ at the beginning of Sec. 7.2. It is not hard to see that $pt$ is stronger than $qt$, and $pe$ is stronger than $qe$, thus every $pt$-frame/model is a $qt$-frame/model, and every $pe$-frame/model is a $qe$-frame/model. We use $\Gamma\vDash_{qt}\varphi$ to mean that $\varphi$ is a semantical consequence of $\Gamma$ over the class of $qt$-frames, that is, for every $qt$-model $\mathcal{M}$ and every state $s$ in $\mathcal{M}$, if $\mathcal{M},s\vDash\psi$ for all $\psi\in\Gamma$, then $\mathcal{M},s\vDash\varphi$. Similar meanings goes to $\Gamma\vDash_{pt}\varphi$, $\Gamma\vDash_{qe}\varphi$, and $\Gamma\vDash_{pe}\varphi$. We will show that ${\bf K4^{\boxdot}}$ is sound and strongly complete with respect to both the class of $qt$-frames and the class of $pt$-frames, and ${\bf K5^{\boxdot}}$ is sound and strongly complete with respect to both the class of $qe$-frames and the class of $pe$-frames.

Before showing the soundness and strong completeness of ${\bf K4^{\boxdot}}$ and ${\bf K5^{\boxdot}}$, it is worth remarking that w$\boxdot 4$ and w$\boxdot 5$ are provable in ${\bf K4^{\boxdot}}$ and ${\bf K5^{\boxdot}}$, respectively, by letting $\psi$ in $\boxdot 4$ and $\boxdot 5$ be $\bot$.

To simplify the proofs below, we provide two useful results.

Proposition 58**.**

Define $\mathcal{M}^{c}$ w.r.t. ${\bf K4^{\boxdot}}$ as in Def. 28 and $sR^{c}_{i}t$ for $i\in\{1,2\}$. If $\boxdot\varphi\in s$, then $\boxdot\varphi\in t$.

Proof.

Suppose that $sR^{c}_{i}t$ for $i\in\{1,2\}$ and $\boxdot\varphi\in s$. Then there exists $\chi$ such that $\neg\boxdot\chi\in s$ and $(\ast)$ for all $\varphi$, if $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$, then $\varphi\in t$.

since $\boxdot\varphi\in s$, by w$\boxdot 4$, we have $\boxdot\boxdot\varphi\in s$; by $\boxdot 4$, we obtain that $\boxdot(\boxdot\varphi\vee\neg\chi)\in s$, that is, $\boxdot(\chi\to\boxdot\varphi)\in s$, then by $(\ast)$, it follows that $\boxdot\varphi\in t$. ∎

Proposition 59**.**

Define $\mathcal{M}^{c}$ w.r.t. ${\bf K5^{\boxdot}}$ as in Def. 28 and $sR^{c}_{i}t$ for $i\in\{1,2\}$. If $\boxdot\varphi\in t$, then $\boxdot\varphi\in s$.

Proof.

Suppose that $sR^{c}_{i}t$ for $i\in\{1,2\}$ and $\neg\boxdot\varphi\in s$. Then there exists $\chi$ such that $\neg\boxdot\chi\in s$ and $(\star)$ for all $\psi$, if $\boxdot\psi\land\boxdot(\chi\to\psi)\in s$, then $\varphi\in t$.

since $\neg\boxdot\varphi\in s$, by w$\boxdot 5$ it follows that $\boxdot\neg\boxdot\varphi\in s$; by $\boxdot 5$, it follows that $\boxdot(\neg\boxdot\varphi\vee\neg\chi)\in s$, i.e. $\boxdot(\chi\to\neg\boxdot\varphi)\in s$. Then using $(\star)$, we derive that $\neg\boxdot\varphi\in t$. ∎

We are now ready to show the soundness and strong completeness of ${\bf K4^{\boxdot}}$ and ${\bf K5^{\boxdot}}$.

Theorem 60**.**

Let $\varphi\in\mathcal{L}(\boxdot)$. The following conditions are equivalent:

• (a)

$\Gamma\vdash_{{\bf K4^{\boxdot}}}\varphi$

• (b)

$\Gamma\vDash_{qt}\varphi$

• (c)

$\Gamma\vDash_{pt}\varphi$.

Proof.

We show $(a)\Rightarrow(b)\Rightarrow(c)\Rightarrow(a)$.

$(a)\Rightarrow(b)$: By soundness of ${\bf K^{\boxdot}}$, it suffices to show that $\boxdot 4$ is valid on the class of $qt$-frames.

If not, there exists a $qt$-model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ and a state $s\in S$ such that $\mathcal{M},s\vDash\boxdot\varphi$ but $s\nvDash\boxdot(\boxdot\varphi\vee\psi)$. Then for some $t$ and $u$, it holds that $sR_{1}t$ and $sR_{2}u$ and $t\vDash\boxdot\varphi\vee\psi\not\Longleftrightarrow u\vDash\boxdot\varphi\vee\psi$. W.l.o.g. we assume that $t\nvDash\boxdot\varphi\vee\psi$ and $u\vDash\boxdot\varphi\vee\psi$. From $t\nvDash\boxdot\varphi\vee\psi$ it follows that $t\nvDash\boxdot\varphi$, and thus there are $v,w$ such that $tR_{1}v$ and $tR_{2}w$ and $(v\vDash\varphi\not\Longleftrightarrow w\vDash\varphi)$. By $sR_{1}t$, $tR_{1}v$, $tR_{2}w$ and the property $(qt)$ of $\mathcal{M}$, we have $sR_{1}v$ and $sR_{2}w$, which together with the fact that $s\vDash\boxdot\varphi$ implies that $(v\vDash\varphi\Longleftrightarrow w\vDash\varphi)$: a contradiction.

$(b)\Rightarrow(c)$: this is because every $pt$-model is a $qt$-model.

$(c)\Rightarrow(a)$: Define $\mathcal{M}^{c}$ w.r.t. ${\bf K4^{\boxdot}}$ as in Def. 28. It is sufficient to show that $\mathcal{M}^{c}$ is a $pt$-model.

Suppose for $i,j\in\{1,2\}$ that $sR^{c}_{i}t$ and $tR_{j}^{c}u$. Then there exists $\chi$ such that $\neg\boxdot\chi\in s$ and (a) for all $\varphi$, if $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$, then $\varphi\in t$, and there is a $\psi$ such that $\neg\boxdot\psi\in t$ and (b) for all $\varphi$, if $\boxdot\varphi\land\boxdot(\psi\to\varphi)\in t$, then $\varphi\in u$. To show $sR_{1}^{c}u$ and $sR^{c}_{2}u$, it suffices to demonstrate that for all $\varphi$, if $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$, then $\varphi\in u$. For this, let $\varphi$ be arbitrary such that $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$. In what follows, we will show that $\boxdot\varphi\land\boxdot(\psi\to\varphi)\in t$, which by (b) implies that $\varphi\in u$.

• •

$\boxdot\varphi\in t$: direct by $sR^{c}_{i}t$ and $\boxdot\varphi\in s$ and Prop. 58.

• •

$\boxdot(\psi\to\varphi)\in t$: from $\boxdot(\chi\to\varphi)\in s$ (i.e. $\boxdot(\neg\varphi\to\neg\chi)\in s$) and $\neg\boxdot\chi\in s$ (i.e. $\boxdot\neg\chi\notin s$), it follows by axiom $\boxdot\text{CON}$ that $\boxdot(\varphi\to\neg\chi)\notin s$, namely $\boxdot(\neg\varphi\vee\neg\chi)\notin s$. Thanks to $\boxdot\varphi\in s$, by axiom $\boxdot\text{DIS}$ we infer that $\boxdot(\varphi\vee\neg\psi)\in s$, that is, $\boxdot(\psi\to\varphi)\in s$. Then by Prop. 58 again, we conclude that $\boxdot(\psi\to\varphi)\in t$.

∎

Theorem 61**.**

Let $\varphi\in\mathcal{L}(\boxdot)$. The following conditions are equivalent:

• (a)

$\Gamma\vdash_{{\bf K5^{\boxdot}}}\varphi$

• (b)

$\Gamma\vDash_{qe}\varphi$

• (c)

$\Gamma\vDash_{pe}\varphi$.

Proof.

We show $(a)\Rightarrow(b)\Rightarrow(c)\Rightarrow(a)$.

$(a)\Rightarrow(b)$: by soundness of ${\bf K^{\boxdot}}$, it is sufficient to show that $\boxdot 5$ is valid on the class of $qe$-frames.

If not, there exists $qe$-model $\mathcal{M}=\langle S,R_{1},R_{2},V\rangle$ and state $s\in S$ such that $\mathcal{M},s\vDash\neg\boxdot\varphi$ but $s\nvDash\boxdot(\neg\boxdot\varphi\vee\psi)$. From $s\vDash\neg\boxdot\varphi$, it follows that for some $t,u$ such that $sR_{1}t$ and $sR_{2}u$ and $t\vDash\varphi\not\Longleftrightarrow u\vDash\varphi$. From $s\nvDash\boxdot(\neg\boxdot\varphi\vee\psi)$, it follows that for some $v,w$ such that $sR_{1}v$ and $sR_{2}w$ and $v\vDash\neg\boxdot\varphi\vee\psi\not\Longleftrightarrow w\vDash\neg\boxdot\varphi\vee\psi$. W.l.o.g. we assume that $v\vDash\neg\boxdot\varphi\vee\psi$ and $w\vDash\boxdot\varphi\land\neg\psi$. By $sR_{2}w$ and $sR_{1}t$ and $sR_{2}u$ and the property $(qe)$ of $\mathcal{M}$, we infer $wR_{1}t$ and $wR_{2}u$. Due to $w\vDash\boxdot\varphi$, we have $t\vDash\varphi\Longleftrightarrow u\vDash\varphi$: a contradiction.

$(b)\Rightarrow(c)$: This is due to the fact that every $pe$-model is a $qe$-model.

$(c)\Rightarrow(a)$: Define $\mathcal{M}^{c}$ w.r.t. ${\bf K5^{\boxdot}}$ as in Def. 28. The remainder is to prove that $\mathcal{M}^{c}$ is a $pe$-model.

Suppose for $i,j\in\{1,2\}$ that $sR^{c}_{i}t$ and $sR^{c}_{j}u$. Then there exists $\chi$ such that $\neg\boxdot\chi\in s$ and $({\dagger})$ for all $\varphi$, if $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$, then $\varphi\in t$, and there is a $\psi$ such that $\neg\boxdot\psi\in s$ and $({\dagger}{\dagger})$ for all $\varphi$, if $\boxdot\varphi\land\boxdot(\psi\to\varphi)\in s$, then $\varphi\in u$. To show $tR^{c}_{1}u$ and $tR^{c}_{2}u$, we need to find a $\delta$ such that $\neg\boxdot\delta\in t$ and for all $\varphi$, if $\boxdot\varphi\land\boxdot(\delta\to\varphi)\in t$, then $\varphi\in u$. We show that $\chi$ is a desired $\delta$.

• •

$\neg\boxdot\chi\in t$: otherwise, by Prop. 59, we would derive $\boxdot\chi\in s$: a contradiction.

• •

Assume for any $\varphi$ such that $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in t$, we only need show that $\varphi\in u$. By assumption and Prop. 59, $\boxdot\varphi\land\boxdot(\chi\to\varphi)\in s$. As $\neg\boxdot\chi\in s$, $\boxdot\neg\chi\notin s$; as $\boxdot(\chi\to\varphi)\in s$, $\boxdot(\neg\varphi\to\neg\chi)\in s$. Thus by axiom $\boxdot\text{CON}$, it follows that $\boxdot(\varphi\to\neg\chi)\notin s$, viz. $\boxdot(\neg\varphi\vee\neg\chi)\notin s$. From this and $\boxdot\varphi\in s$ and axiom $\boxdot\text{DIS}$, we have $\boxdot(\varphi\vee\neg\psi)\in s$, that is, $\boxdot(\psi\to\varphi)\in s$. Now applying $({\dagger}{\dagger})$, we get $\varphi\in u$, as desired.

∎

8 Conclusion and Future work

In this paper, we proposed the operator $\boxdot$ for the generalized noncontingency and the operator $\boxplus$ for pseudo noncontingency, which are obtained by slightly adapting two equivalent semantics of noncontingency operator. We showed that $\mathcal{L}(\boxdot)$ is less expressive than $\mathcal{L}(\boxplus)$ over five basic model classes. Besides, the two logics cannot define the five basic frame properties, with the aid of a notion of $\boxdot$-morphisms. We then presented the minimal logic of $\mathcal{L}(\boxplus)$, which also characterizes the class of serial bimodal frames. Moreover, we axiomatized $\mathcal{L}(\boxdot)$ over various frame classes, among which the completeness of serial logic and of symmetric logic were shown via the notion of $\boxdot$-morphisms.

There are a lot of future work to be continued. For instance, the axiomatizations of $\mathcal{L}(\boxplus)$ over the class of frames with other special properties, including reflexivity, transitivity, symmetry, Euclidicity; the axiomatizations of $\mathcal{L}(\boxdot)$ over the class of transitive frames and over the class of Euclidean frames.

Acknowledgements

This research is financially supported by the project 17CZX053 of National Social Science Fundation of China.