A Note on the Issue of Cohesiveness in Canonical Models

Abstract

In their presentation of canonical models for normal systems of modal logic, Hughes and Cresswell observe that some of these models are based on a frame which can be also thought of as a collection of two or more isolated frames; they call such frames ‘non-cohesive’. The problem of checking whether the canonical model of a given system is cohesive is still rather unexplored and no general decision procedure is available. The main contribution of this article consists in introducing a method which is sufficient to show that canonical models of some relevant classes of normal monomodal and bimodal systems are always non-cohesive.

1 Introduction

The canonical model construction is a standard technique to prove completeness results in modal logic. In the case of normal modal systems the canonical model is based on a relational frame (a set of states, each corresponding to a maximally consistent set of formulas, and accessibility relations among them); thus, a natural question is whether that frame can be also thought of as a collection of at least two isolated frames or not. According to the terminology in Hughes and Cresswell (1984, 1996), we will say that a frame which does not correspond to a collection of at least two isolated frames is cohesive.¹ There is currently no uniform method to check whether the canonical model of a given normal system is based on a cohesive frame and this problem is rather unexplored, despite the fact that completeness theory represents one of the main areas of research in theoretical modal logic. In particular, it is interesting to check whether it is possible to find syntactic or semantic properties of classes of systems that are sufficient to guarantee cohesiveness or non-cohesiveness of canonical models.

For instance, Hughes and Cresswell (1996) provide a strategy which can be described as follows: one assumes that the canonical model of a system S includes a state w which has access to all other states of the domain; if this assumption does not conflict with the properties of the canonical model of S, then the underlying frame is obviously cohesive. However, such an assumption is very strong and the fact that it conflicts with the properties of the canonical model of a system S is not sufficient to claim that the underlying frame is non-cohesive (a frame can be cohesive even if there is no state having access to all the others). The main contribution of the present article consists in providing a sort of complementary strategy, which can be called the method of isolated worlds: we check whether the canonical model of a system S includes a state w such that (I) w has no access to any state (with the possible exception of itself) and (II) no state has access to w (with the possible exception of itself). If this is the case, then the canonical model is clearly based on a non-cohesive frame. We will see that canonical models of relevant classes of normal monomodal and bimodal systems include states of such kind. Therefore, the described strategy will allow us to shed further light on the issue of cohesiveness.

The article is organized as follows: in Sect. 2 we introduce the fundamental notions involved in our inquiry; in Sect. 3 we recall and extend results obtained with methods proposed by Hughes and Cresswell; in Sect. 4 we illustrate some results obtained with the method of isolated worlds; finally, in Sect. 5 we provide some directions for future research.

2 Preliminary Notions

Consider a countable set of propositional variables VAR, denoted by p, q, r, etc. and let $\mathcal {L}_\square$ be the language over VAR obtained by means of the boolean operators $\lnot$ and $\rightarrow$ and the (monadic) modal operator $\square$; furthermore, let $\mathcal {L}_{\square \blacksquare }$ be obtained from $\mathcal {L}_\square$ by adding to its primitive symbols the (monadic) modal operator $\blacksquare$. Hereafter, we will refer to $\mathcal {L}_\square$ as the monomodal language (over VAR) and to $\mathcal {L}_{\square \blacksquare }$ as the bimodal language (over VAR). We adopt standard definitions to use in our languages also some non-primitive boolean and modal operators, such as $\wedge$, $\vee$, $\equiv$, $\bot$, $\top$, $\lozenge$ (both in $\mathcal {L}_\square$ and $\mathcal {L}_{\square \blacksquare }$) and $\blacklozenge$ (only in $\mathcal {L}_{\square \blacksquare }$). It is convenient to just recall that $\lozenge$ is an abbreviation for $\lnot \square \lnot$ and $\blacklozenge$ an abbreviation for $\lnot \blacksquare \lnot$. In the present article we restrict our attention to the two languages described: in particular, the bimodal language is at the basis of systems of tense logic, which will play a relevant role in our presentation.

The language $\mathcal {L}_\square$ is interpreted in monomodal relational frames, which are structures of kind $\mathfrak {F}=\langle W,R_\square \rangle$, where W is a non-empty domain of states or worlds (denoted by w, v, u, etc.) and $R_\square \subseteq W\times W$ a relation that can be called $\square$-accessibility. The language $\mathcal {L}_{\square \blacksquare }$ is interpreted in bimodal relational frames, which are structures of kind $\mathfrak {F}=\langle W,R_\square ,R_\blacksquare \rangle$, where W and $R_\square$ are defined as before and $R_\blacksquare \subseteq W\times W$ is a relation that can be called $\blacksquare$-accessibility. For any world $w\in W$, we can say that $R_\square (w)=\{u\in W:wR_\square u\}$ is the $\square$-accessibility sphere of w and $R_\blacksquare (w)=\{u\in W:wR_\blacksquare u\}$ is the $\blacksquare$-accessibility sphere of w. If $R_\square (w)=\emptyset$ or $R_\blacksquare (w)=\emptyset$, we can say that w is $R_\square$-blind or, respectively, $R_\blacksquare$-blind. We will adapt some terminology in Segerberg (1971) in order to make reference to particular kinds of worlds in a frame. We will say that a world w is a degenerate cluster if and only if (hereafter, iff):

• $\forall x \in W \lnot (w R x)$, for every relation R in the frame of w.

Furthermore, we will say that a world w is a simple cluster iff:

• $\forall x \in W ((w R x) \equiv (x=w))$, for every relation R in the frame of w.

Accessibility relations can be used to define accessibility walks in frames.

Definition 2.1

In a monomodal (bimodal) frame an accessibility walk is a sequence of states $(w_0,...,w_n)\in W^{n+1}$ s.t. $n>0$ and $w_iR_\square w_{i+1}$ (either $w_iR_\square w_{i+1}$ or $w_iR_\blacksquare w_{i+1}$) for each $i<n$. Such a walk is said to be of length n and from$w_0$to$w_n$. Given two states w and v in a frame, if there is an accessibility walk of length n from w to v, then we say that w has access to v in $n R_\square$-steps (in $n (R_\square \cup R_\blacksquare )$-steps).

For the aims of the present article it is fundamental to introduce also the notion of a pseudo-accessibility walk.

Definition 2.2

In a monomodal (bimodal) frame a pseudo-accessibility walk is a sequence of states $(w_0,...,w_n)\in W^{n+1}$ s.t. $n\ge 0$ and either $w_i R_\square w_{i+1}$ or $w_{i+1} R_\square w_i$ (either $w_i R_\square \cup R_\blacksquare w_{i+1}$ or $w_{i+1} R_\square \cup R_\blacksquare w_i$) for each $i<n$. Such a walk is said to be of length n and from$w_0$to$w_n$. Given two states w and v in a frame, if there is a pseudo-accessibility walk of length n from w to v, then we say that w has pseudo-access to v in $n (R_\square \cup R_\square ^{-1})$-steps, where $R^{-1}_\square$ is the converse of $R_\square$ (in $n (R_\square \cup R_\square ^{-1}\cup R_\blacksquare \cup R_\blacksquare ^{-1})$-steps, where $R^{-1}_\blacksquare$ is the converse of $R_\blacksquare$).

Notice that the reverse of a pseudo-accessibility walk from w to u is a pseudo-accessibility walk from u to w; therefore, we will sometimes simply say that there is a pseudo-accessibility walk betweenw and u. Furthermore, according to Definition 2.2, a world has always pseudo-access to itself in some number of steps $n\ge 0$.

A frame including a state w s.t. for any state $v\ne w$ in the domain there is an accessibility walk from w to v is said to be generated (by w). A monomodal (bimodal) frame including a state w s.t. for any state $v\ne w$ in the domain we have $w R_\square v$ ($w R_\square v$ or $w R_\blacksquare v$) is said to be strongly generated (by w). We will adopt the convention that frames denoted by $\mathfrak {F}$, $\mathfrak {F}_i$, etc. respectively have the structure $\mathfrak {F}=\langle W, R_\square \rangle$ ($\mathfrak {F}=\langle W, R_\square ,R_{\blacksquare }\rangle$ in the bimodal case), $\mathfrak {F}_i=\langle W_i, R_{i\square }\rangle$ ($\mathfrak {F}_i=\langle W_i, R_{i\square }, R_{i\blacksquare }\rangle$ in the bimodal case), etc.

Another important notion is that of an amalgamation of a class of frames, introduced in Hughes and Cresswell (1984) for the monomodal case.

Definition 2.3

Given a finite class of frames $C_f=\{\mathfrak {F}_1$,..., $\mathfrak {F}_n\}$ whose domains are pairwise disjoint, an amalgamation of $C_f$ is a frame $\mathfrak {F}^*=\langle W^*, R^*_\square \rangle$ satisfying the following conditions (where $w^*\notin W_1\cup ...\cup W_n$):

• $W^*=W_1\cup ...\cup W_n\cup \{w^*\}$;

• for any $w,v\in W_i$ s.t. $1\le i\le n$, $wR^*_\square v$ iff $wR_{i\square } v$;

• for any $w\in W_i$ s.t. $1\le i\le n$, $w^*R^*_\square w$;

• for any $w\in W_i$ and $v\in W_j$ s.t. $1\le i,j \le n$ and $i\ne j$, $\lnot (w R^*_\square v)$.

We will say that $w^*$ is the characteristic world of the amalgamation. Notice that there are exactly two amalgamations for any finite class of monomodal frames: the one in which $w^* \in R^*_\square (w^*)$ and the one in which $w^*\notin R^*_\square (w^*)$. The amalgamation of a finite class of monomodal frames is a strongly generated frame (by $w^*$); thus, the natural way of adapting the definition of amalgamation to a finite class of bimodal frames consists in replacing the last three clauses of Definition 2.3 with:

• for any $w,v\in W_i$ s.t. $1\le i\le n$, $wR^*_\square v$ iff $wR_{i\square } v$ and $wR^*_\blacksquare v$ iff $wR_{i\blacksquare } v$;

• for any $w\in W_i$ s.t. $1\le i\le n$, either $w^*R^*_\square w$ or $w^*R^*_\blacksquare w$;

• for any $w\in W_i$ and $v\in W_j$ s.t. $1\le i,j \le n$ and $i\ne j$, $\lnot (w R^*_\square v)$ and $\lnot (w R^*_\blacksquare v)$.

A model over a (monomodal or bimodal) relational frame is a structure of kind $\mathfrak {M}=\langle \mathfrak {F},V\rangle$, where $\mathfrak {F}$ is the underlying frame and $V:VAR\longrightarrow \wp (W)$ is a valuation function. We will adopt the convention that models denoted by $\mathfrak {M}$, $\mathfrak {M}_i$, etc. respectively have the structure $\mathfrak {M}=\langle \mathfrak {F}, V\rangle$, $\mathfrak {M}_i=\langle \mathfrak {F}_i, V_i\rangle$, etc.

Truth-conditions are stated below (those concerning formulas of kind $\blacksquare \phi$ apply, of course, only to models over bimodal frames):

• $\mathfrak {M},w\vDash p$ iff $w\in V(p)$, for any $p\in VAR$;

• $\mathfrak {M},w \vDash \lnot \phi$ iff $\mathfrak {M},w\nvDash \phi$;

• $\mathfrak {M},w\vDash \phi \rightarrow \psi$ iff $\mathfrak {M},w\nvDash \phi$ or $\mathfrak {M},w\vDash \psi$;

• $\mathfrak {M},w\vDash \square \phi$ iff for every $v\in R_\square (w)$, $\mathfrak {M},v\vDash \phi$;

• $\mathfrak {M},w\vDash \blacksquare \phi$ iff for every $v\in R_\blacksquare (w)$, $\mathfrak {M},v\vDash \phi$.

The notion of validity for formulas is defined in the usual way. A formula $\phi \in \mathcal {L}_\square$ ($\phi \in \mathcal {L}_{\square \blacksquare }$) is valid in a model $\mathfrak {M}$ iff $\mathfrak {M},w\vDash \phi$ for every $w\in W$ (we represent this fact as $\mathfrak {M}\vDash \phi$); $\phi$ is valid in a class of models $C_m$ iff $\mathfrak {M}\vDash \phi$ for every $\mathfrak {M}\in C_m$ (we represent this fact as $C_m\vDash \phi$); $\phi$ is valid in a frame $\mathfrak {F}$ iff $\mathfrak {M}\vDash \phi$ for every $\mathfrak {M}$ over $\mathfrak {F}$ (we represent this fact as $\mathfrak {F}\vDash \phi$); finally, $\phi$ is valid in a class of frames $C_f$ iff $\mathfrak {F}\vDash \phi$ for every $\mathfrak {F}\in C_f$ (we represent this fact as $C_f\vDash \phi$).

Definition 2.4

A model $\mathfrak {M}^*=\langle \mathfrak {F}^*,V^*\rangle$ is an amalgamation of a finite class of models $C_m=\{ \mathfrak {M}_1,...,\mathfrak {M}_n\}$ iff $\mathfrak {F}^*$ is an amalgamation of the frames of the models in $C_m$ and for every $p\in VAR$ and $v\in W_i$ (where $1\le i\le n$), $v\in V^*(p)$ iff $v\in V_i(p)$.

The definition of an amalgamation of a finite class of models in the bimodal case is analogous. When $C_m=\{\mathfrak {M}\}$, we will speak of the amalgamation of $\mathfrak {M}$, for the sake of brevity.

Logical systems will be specified in terms of an axiomatic basis over $\mathcal {L}_\square$ or $\mathcal {L}_{\square \blacksquare }$. Any logical system considered here includes all theorems of the classical propositional calculus (PC) and is closed under Modus Ponens; thus, for any system S, we have the following two principles:

PC   :

if $\vdash _{\mathbf{PC}}\phi$, then $\vdash _S\phi '$, where $\phi '$ is any substitution instance of $\phi$;

RMP:

if $\vdash _S\phi$ and $\vdash _S\phi \rightarrow \psi$, then $\vdash _S\psi$.

A system of monomodal logic S is normal iff it is closed under the following principles:

$K_\square$   :

$\square (\phi \rightarrow \psi )\rightarrow (\square \phi \rightarrow \square \psi )$;

$RN_\square$:

if $\vdash _S{\phi }$ then $\vdash _S{\square \phi }$.

A system of bimodal logic is normal iff it is closed under $K_\square$, $RN_\square$ and the following principles:

$K_\blacksquare$   :

$\blacksquare (\phi \rightarrow \psi )\rightarrow (\blacksquare \phi \rightarrow \blacksquare \psi )$;

$RN_\blacksquare$:

if $\vdash _S{\phi }$ then $\vdash _S{\blacksquare \phi }$.

Given a formula $\phi \in \mathcal {L}_{\square \blacksquare }$, the formula $\phi ^{mi}$, which can be called the mirror image of$\phi$, is the result of simultaneously replacing in $\phi$ each occurrence of a ‘white modal operator’ ($\square$ and $\lozenge$) with an occurrence of the corresponding ‘black modal operator’ ($\blacksquare$ and $\blacklozenge$) and vice versa; for instance, $(\square \lozenge p\rightarrow \blacklozenge \lozenge p)^{mi}= \blacksquare \blacklozenge p\rightarrow \lozenge \blacklozenge p$. It follows from this definition that for all $\phi \in \mathcal {L}_{\square \blacksquare }$, $(\phi ^{mi})^{mi}=\phi$. We can also speak of the mirror image of a schema of formulas; for instance, $K_\square$ is the mirror image of $K_\blacksquare$ and vice versa.² A normal bimodal system S has the mirror image property iff it is closed under the following rule:

RMI:

if $\vdash _S{\phi }$ then $\vdash _S{\phi ^{mi}}$.

Bimodal systems with the mirror image property will be also called mirror systems. A bridge-schema in a bimodal language is a schema including at least one occurrence of a ‘white modal operator’ and at least one occurrence of a ‘black modal operator’. If the axiomatic basis of a bimodal system S does not involve any bridge-schema, then we can say that it is a separable axiomatic basis (Catach 1988). A mirror system S whose axiomatic basis is separable can be said to be the duplication of a monomodal system. Finally, a normal bimodal system is a system of tense logic iff it is closed under the following bridge-schemata:

BR1:

$\phi \rightarrow \square \blacklozenge \phi$;

BR2:

$\phi \rightarrow \blacksquare \lozenge \phi$;

In order to speak of the properties of a generic (monomodal or bimodal) system S, we can denote its language by $\mathcal {L}(S)$. A system S is sound with respect to (w.r.t.) a class of models $C_m$ iff, for every $\phi \in \mathcal {L}(S)$, $\vdash _S\phi$ entails $C_m\vDash \phi$; S is complete w.r.t $C_m$ iff, for every $\phi \in \mathcal {L}(S)$, $C_m\vDash \phi$ entails $\vdash _S\phi$. Finally S is characterized by $C_m$ iff it is both sound and complete w.r.t. $C_m$. Analogous definitions can be used for soundness, completeness and characterization of a system in terms of a class of frames.

Let us use the notation $\mathbf{K }_\square$ for the weakest normal monomodal system and $\mathbf{K }_{\square \blacksquare }$ for the weakest normal bimodal system. $\mathbf{K }_{\square \blacksquare }$ is the duplication of $\mathbf{K }_\square$. It is well-known that $\mathbf{K }_\square$ and $\mathbf{K }_{\square \blacksquare }$ are respectively characterized by the class of all monomodal frames and the class of all bimodal frames. The weakest normal system of tense logic will be denoted by $\mathbf{K }_t$, as it is commonly done in the literature.³ In general, we will use standard names for systems of monomodal and bimodal logic; sometimes we will also denote extensions of a system S by means of the expression $S+\{X_1,...,X_n\}$ where $X_1,...,X_n$ are labels for axiom-schemata, meaning that $S+\{X_1,...,X_n\}$ is the result of extending the axiomatic basis of S with the axiom-schemata $X_1,...,X_n$.⁴ Finally, in the case of a bimodal system S with a separable axiomatic basis, we will follow Kurucz (2007) and denote S also as $S'\otimes S''$, where $S'$ is the subsystem of S providing the axiomatization of $\square$ and $S''$ the subsystem of S providing the axiomatization of $\blacksquare$. The system $\mathbf{K }_t$$=$K$_{\square \blacksquare }+\{BR1, BR2\}$ is characterized by the class of all bimodal frames in which $R_\square$ and $R_\blacksquare$ are reciprocally converse relations, namely by the class of frames satisfying the following property:

$$\begin{aligned} \forall w,v\in W (v\in R_\square (w)\equiv w\in R_\blacksquare (v)) \end{aligned}$$

A system S is consistent iff $\nvdash _S\bot$; a formula $\phi \in \mathcal {L}(S)$ is consistent with a system S, or S-consistent, iff $\nvdash _S\lnot \phi$; a set of formulas $\Gamma \subset \mathcal {L}(S)$ is S-consistent iff there is no finite $\Gamma '=\{\phi _1,...,\phi _n\}\subseteq \Gamma$ s.t. $\vdash _S\lnot (\phi _1\wedge ...\wedge \phi _n)$; $\Gamma$ is a maximally S-consistent set of formulas iff $\Gamma$ is S-consistent and there is no $\Gamma '$ s.t. $\Gamma \subset \Gamma '$ and $\Gamma '$ is S-consistent. If $\Gamma$ is a maximally S-consistent set of formulas, then $Th(S)=\{\psi \in \mathcal {L}(S): \vdash _S\psi \}\subseteq \Gamma$. If $\phi$ is S-consistent, then there is a maximally S-consistent set of formulas including $\phi$; finally, if $\Gamma$ is S-consistent, then there is a maximally S-consistent set of formulas containing $\Gamma$.

A system S is a subsystem of (or is contained in) a system $S'$ iff $Th(S)\subseteq Th(S')$. If S is a subsystem of $S'$, then $S'$ is an extension of (or contains) S. If S is a subsystem of $S'$ and an extension of $S''$, we will say that S is between$S'$ and $S''$.

Consider the following principles:

$Ver_\square$   :

$\square \phi$;

$Triv_\square$:

$\square \phi \equiv \phi$.

According to a fundamental result in Makinson (1971), any consistent normal monomodal system is either a subsystem of $\mathbf{Ver }_\square = \mathbf{K }_\square + \{Ver_\square \}$ or a subsystem of $\mathbf{Triv }_\square = \mathbf{K }_\square + \{Triv_\square \}$, since these are the only two maximally normal monomodal systems (i.e., systems having no consistent normal extension, see Goldblatt and Kowalski 2014). In particular, we have that, for any consistent normal modal system S, $Th(S)\subseteq Th(\mathbf Ver _\square )$ iff $\nvdash _S\lozenge \top$, while $Th(S)\subseteq Th(\mathbf Triv _\square )$ if $\vdash _S\lozenge \top$ (but not conversely). Both $\mathbf{Triv }_\square$ and $\mathbf{Ver }_\square$ are closed under the following schema, which will be taken into account later:

$Tc_\square$:

$\phi \rightarrow \square \phi$.

On the other hand, if $Ver_\blacksquare$ and $Triv_\blacksquare$ stand for the mirror images of $Ver_\square$ and $Triv_\square$, then there are consistent normal bimodal systems which are neither subsystems of $\mathbf{Ver }_{\square \blacksquare }$$=$$\mathbf{K }_{\square \blacksquare }$$+ \{Ver_\square , Ver_\blacksquare \}$ nor subsystems of $\mathbf{Triv }_{\square \blacksquare } = \mathbf{K }_{\square \blacksquare } + \{Triv_\square , Triv_\blacksquare \}$; very simple examples are $\mathbf{K }_{\square \blacksquare } + \{Ver_\square , Triv_\blacksquare \}$ and $\mathbf{K }_{\square \blacksquare } + \{Triv_\square , Ver_\blacksquare \}$. Indeed, as shown in Williamson (1998), there are continuum many maximally normal bimodal systems.

Many interesting systems of tense logic have the mirror image property and are either contained in $\mathbf{Ver }_{\square \blacksquare }$ or in $\mathbf{Triv }_{\square \blacksquare }$. However, there are also interesting systems of tense logic lacking the mirror image property and that are neither contained in $\mathbf{Ver }_{\square \blacksquare }$ nor in $\mathbf{Triv }_{\square \blacksquare }$; for instance, a system discussed by Thomason (1972), which is not characterized by any class of temporal frames,⁵ and systems used to represent asymmetries in time, such as ${\mathbf{K}}_b = {\mathbf{K}}_t + \{4_\square , 4_\blacksquare ,(\blacksquare (\phi \vee \psi )\wedge \blacksquare (\phi \vee \blacksquare \psi )\wedge \blacksquare (\blacksquare \phi \vee \psi )) \rightarrow (\blacksquare \phi \vee \blacksquare \psi )\}$ for transitive and past-linear time.

Given a normal system of monomodal (respectively, bimodal) logic S, the canonical frame of S is the frame $\mathfrak {F}^S=\langle W^S,R_\square ^S\rangle$ (respectively, the frame $\mathfrak {F}^S=\langle W^S,R_\square ^S, R_\blacksquare ^S\rangle$) where $W^S$ is the set of all maximally S-consistent sets of formulas and, for any $w,v\in W^S$, $wR_\square ^Sv$ iff $\square ^-(w)=\{\phi :\square \phi \in w\}\subseteq v$ (also, $wR_\blacksquare ^Sv$ iff $\blacksquare ^-(w)=\{\phi :\blacksquare \phi \in w\}\subseteq v$). Given a formula $\phi \in \mathcal {L}(S)$, let $|\phi |^{\mathfrak {F}^S}=\{w\in W^S: \phi \in w\}$. The canonical model of S is the model $\mathfrak {M}^S=\langle \mathfrak {F}^S,V^S\rangle$ s.t. $\mathfrak {F}^S$ is the canonical frame of S and, for any $p\in VAR$, $V(p)=|p|^{\mathfrak {F}^S}$. It is well-known that canonical models have the following property (Truth Lemma):⁶

• for any $w\in W^S$ and any $\phi \in \mathcal {L}(S)$, $\mathfrak {M}^S,w\vDash \phi$ iff $w\in |\phi |^{\mathfrak {F}^S}$.

It is also well-known that any consistent normal modal system is characterized by its canonical model, though not necessarily by its canonical frame, as it is witnessed by the aforementioned system in Thomason (1972).

3 Some Remarks on Hughes and Cresswell’s Analysis of Cohesiveness

In the previous section we provided all relevant notions for our inquiry except the crucial one, that of a cohesive frame, which is stated below and based on the idea of a pseudo-accessibility walk between a pair of states in a frame:

Definition 3.1

A relational frame is cohesive iff there is a pseudo-accessibility walk between any pair of states in its domain.

Hughes and Cresswell (1996) observe that one way of deciding whether the canonical model of a monomodal system S is cohesive (i.e., is based on a cohesive frame) consists in checking whether there is a maximally S-consistent set of formulas which strongly generates the frame. This strategy can be more precisely described in terms of amalgamations. One takes the canonical model of a system S and creates an amalgamation $\mathfrak {M}^*$ of it (namely, of the singleton $\{\mathfrak {M}^S\}$). Due to the properties of canonical models, if $w^*$ is the characteristic world of the amalgamation, then we have that, for all $\phi \in \mathcal {L}_\square$, $\mathfrak {M}^*,w^*\vDash \square \phi$ only if $\vdash _S\phi$. Next, one checks whether $\mathfrak {M}^*$ is a model for S; if this is the case, the previous claim can be strengthened by saying that, for all $\phi \in \mathcal {L}_\square$, $\mathfrak {M}^*,w^*\vDash \square \phi$ if and only if $\vdash _S\phi$. From this one can infer that $\{\lnot \square \phi {:}\nvdash _S\phi \}$ is an S-consistent set of formulas and can be extended to a maximally S-consistent set of formulas w which belongs to the domain of $\mathfrak {M}^S$. Finally, due to the properties of canonical models, w is a strongly generating world in $\mathfrak {M}^S$.

A related strategy can be found in Hughes and Cresswell (1984), where it is shown that the canonical model of a monomodal system S is built over a cohesive frame whenever S is closed under the following Rule of Disjunction:

$RDis_\square$:

if $\vdash _S\square \phi _1\vee ...\vee \square \phi _n$, then $\vdash _S\phi _i$, for some i s.t. $1\le i \le n$.

Theorem 6.5 in Hughes and Cresswell (1984) shows that if S is a normal modal system closed under $RDis_\square$, then the canonical model of S includes a strongly generating world. Furthermore, as a consequence of Corollary 5.7 and Theorem 6.6 in Hughes and Cresswell (1984), if for every finite collection of generated submodels of the canonical model of a normal system S there is an amalgamation which is also a model for S, then S is closed under $RDis_\square$.

Relying on the methods described, Hughes and Cresswell are able to prove that the canonical models of the systems $\mathbf{K }_\square$, $\mathbf{KD}_\square$, $\mathbf{KT}_\square$, $\mathbf{K4}_\square$ and $\mathbf{S4}_\square$ are cohesive. Their results can be extended by looking at correspondence theory (van Benthem 1983); here we illustrate some examples putting at work the various methods.

Consider the schema below:

$F_\square$:

$(\square \lozenge \phi \wedge \square \lozenge \psi )\rightarrow \lozenge (\phi \wedge \psi )$.

The property of $R_\square$ associated with $F_\square$, called finality, is the following:

$$\begin{aligned} \forall w\exists w'(wR_\square w' \wedge \forall w''(w'R_\square w'' \rightarrow w' = w'')) \end{aligned}$$

Informally, this property means that every world has access to at least one simple cluster. Take the canonical model of $\mathbf{KF }_\square$, that is $\mathbf K + \{F_\square \}$, and build an amalgamation $\mathfrak {M}^*$ of it. Let $w^*$ be the characteristic world of the amalgamation. We need to check whether $\mathfrak {M}^*$ is a model for $\mathbf{KF }_\square$. One way of doing this is looking at the properties of the underlying frame; now, since $w^*$ has access to all simple clusters in $\mathfrak {M}^\mathbf{KF _\square }$, then finality holds for the relation $R^*_\square$ in the frame of $\mathfrak {M}^*$, which is therefore a model for $\mathbf{KF }_\square$. From this one can infer that, for all $\phi \in \mathcal {L}_\square$, $\mathfrak {M}^*,w^*\vDash \square \phi$ if and only if $\vdash _S\phi$; the cohesiveness of $\mathfrak {M}^\mathbf{KF _\square }$ follows from the fact that $\{\lnot \square \phi {:} \nvdash _\mathbf{KF _\square }\phi \}$ is a $\mathbf{KF }_\square$-consistent set of formulas and thus can be extended to a maximally $\mathbf{KF }_\square$-consistent set of formulas w which is, by construction, a strongly generating world in $\mathfrak {M}^\mathbf{KF _\square }$.

The cases of $\mathbf{KD }_\square +\{F_\square \}$ and $\mathbf{K4 }_\square +\{F_\square \}$ are analogous, since the frame of an amalgamation is always serial and transitive when the frames in the class being amalgamated are themselves serial and transitive. In the cases of $\mathbf{KT }_\square +\{F_\square \}$ and $\mathbf{S4 }_\square +\{F_\square \}$ the argument used for $\mathbf{KF }_\square$ only requires the addition that $w^*R^*_\square w^*$. Similarly, consider the following schema:

$4c_\square$:

$\square \square \phi \rightarrow \square \phi$.

Take an amalgamation $\mathfrak {M}^*$ of the canonical model of the system $\mathbf{K4c }_\square = \mathbf{K }_\square + \{4c_\square \}$ s.t. $w^*R^*_\square w^*$, where $w^*$ is the characteristic world of the amalgamation. The frame of $\mathfrak {M}^*$ satisfies the property of $R_\square$ associated with $4c_\square$, that is density:

$$\begin{aligned} \forall w,v(wR_\square v\rightarrow \exists u(wR_\square u \wedge u R_\square v)) \end{aligned}$$

Indeed, it is sufficient to observe that $w^*R^*_\square w^*$ guarantees that for every world $v\in W^*$ there is a world ($w^*$) which is accessible from $w^*$ and has access to v. Thus, the cohesiveness of $\mathbf{K4c }_\square$ follows in the usual way.

As it is illustrated in Chagrov and Zakharyaschev (1997), the systems $\mathbf K4 _\square +\{F_\square \}$ and $\mathbf S4 _\square +\{F_\square \}$ are actually equivalent to the systems obtained by adding respectively to $\mathbf{K4 }_\square$ and $\mathbf{S4 }_\square$ the McKinsey-schema:

$M_\square$:

$\square \lozenge \phi \rightarrow \lozenge \square \phi$.

At this point one may wonder whether the system obtained by adding $M_\square$ directly to $\mathbf{K }_\square$, that is $\mathbf{KM }_\square$, has a cohesive canonical model as well. This is indeed the case. Take any finite collection $C_m$ of generated submodels of the canonical model of $\mathbf{KM }_\square$. Let $\mathfrak {M}^*$ be an amalgamation of $C_m$ and assume that it is not a model for $\mathbf{KM }_\square$. Then, it must be the case that for some formula $\psi$, $\square \lozenge \psi \rightarrow \lozenge \square \psi$ is false at $w^*$ in $\mathfrak {M}^*$, where $w^*$ is the characteristic world of the amalgamation. This means that both $\square \lozenge \psi$ and $\square \lozenge \lnot \psi$ are true at $w^*$, hence that $\lozenge \psi$ and $\lozenge \lnot \psi$ are true at every world of a model in $C_m$; from this one can infer that $\square \lozenge \psi$ and $\square \lozenge \lnot \psi$ are true at every such world and so are $\lozenge \square \psi$ and $\lozenge \square \lnot \psi$, due to applications of $M_\square$, which is valid in $C_m$. However, since $\lozenge \square \lnot \psi$ is equivalent to $\lnot \square \lozenge \psi$, then every world in $C_m$ turns out to be inconsistent, contrarily to the assumption. Hence $\mathfrak {M}^*$ is a model for $\mathbf{KM }_\square$ and $\mathbf{KM }_\square$ is closed under $RDis_\square$, so its canonical model is cohesive.

Hughes and Cresswell notice also that the canonical models of the systems $\mathbf{Ver }_\square$, $\mathbf{Triv }_\square$ and $\mathbf{S5}_\square$ are non-cohesive. In the first two cases the result is straightforward, given that the canonical model of $\mathbf{Ver }_\square$ includes only degenerate clusters and the canonical model of $\mathbf{Triv }_\square$ includes only simple clusters; in the third case the result relies on the fact that if the canonical model of $\mathbf{S5}_\square$ were cohesive it would also be strongly generated by every world (since $R_\square$ would be a universal relation) and this, in turn, would entail that $\lozenge p\in Th({\mathbf{S5}_\square })$ for every $p\in VAR$, which is clearly not the case.

We provide here also a bimodal version of the Rule of Disjunction and illustrate that it entails the existence of a strongly generating world in the canonical model as well:

• $RDis_{\square \blacksquare }$ if $\vdash _S(\square \phi _1\wedge \blacksquare \phi _1)\vee ...\vee (\square \phi _n\wedge \blacksquare \phi _n)$, then $\vdash _S\phi _i$, for some i s.t. $1\le i \le n$.

Proposition 3.2

Given a normal bimodal system S, if S is closed under the rule $RDis_{\square \blacksquare }$, then $\mathfrak {M}^S$ is strongly generated.

Proof

Assuming that the set $\{\lnot (\square \phi \wedge \blacksquare \phi ){:}\nvdash _S\phi \}$ is not S-consistent, one gets that $\vdash _S\lnot (\lnot (\square \phi _1\wedge \blacksquare \phi _1)\wedge ...\wedge \lnot (\square \phi _n\wedge \blacksquare \phi _n))$ for some $\phi _1,...,\phi _n$ which are not in Th(S). Therefore, $\vdash _S(\square \phi _1\wedge \blacksquare \phi _1)\vee ...\vee (\square \phi _n\wedge \blacksquare \phi _n)$ and so, by $RDis_{\square \blacksquare }$, $\vdash _S\phi _i$ for some i s.t. $1\le i\le n$, contrarily to the assumption. This means that $\{\lnot (\square \phi \wedge \blacksquare \phi ){:}\nvdash _S\phi \}$ is S-consistent and can be extended to a maximally S-consistent set w s.t., for all $\psi \in \mathcal {L}_{\square \blacksquare }$, $\square \psi \wedge \blacksquare \psi \in w$ if and only if $\vdash _S\psi$. Take an arbitrary world $v\in W^S$ and suppose that $\lnot (w R_\square v)$ and $\lnot (w R_\blacksquare v)$. Then there are formulas $\square \phi ,\blacksquare \psi \in w$ with $\phi ,\psi \notin v$. Let $\theta =\phi \vee \psi$. Then $\square \theta \wedge \blacksquare \theta \in w$. From this we can infer $\vdash _S\theta$ and so $\theta \in v$; but this entails that either $\phi \in v$ or $\psi \in v$: contradiction. Therefore, we can conclude that w is a strongly generating world in $\mathfrak {M}^S$. $\square$

An important issue, which is left open by Hughes and Cresswell, is whether there is a correspondence between the fact that a system S is closed under $RDis_\square$ (or $RDis_{\square \blacksquare }$) and the fact that the canonical model of S is based on a strongly generated frame. One can show that this is actually the case.

Proposition 3.3

Any strongly generating world w in the canonical model of a monomodal system S is such that $wR^S_\square w$. Furthermore, any strongly generating world v in the canonical model of a bimodal system $S'$ is such that either $vR^{S'}_\square v$ or $vR^{S'}_\blacksquare v$.

Proof

In the monomodal case, suppose that w is a strongly generating world in $\mathfrak {M}^S$ and that $\lnot (wR^S_\square w)$. Then, for some formula $\psi$, we have $\square \psi ,\lnot \psi \in w$. From this we can infer that $\psi \in u$ for every world u s.t. $u\ne w$ and so that w is the unique world in $\mathfrak {M}^S$ s.t. $\lnot \psi \in w$. However, this cannot be the case, since, for every propositional variable p not in $\psi$, both sets $\{\lnot \psi , p\}$ and $\{\lnot \psi , \lnot p\}$ are S-consistent and so they can be extended to two maximally S-consistent sets of formulas corresponding to two different worlds in $\mathfrak {M}^S$. Therefore, there is no formula $\psi$ s.t. $\square \psi ,\lnot \psi \in w$ and this entails that $wR^S_\square w$, contrarily to the hypothesis.

In the bimodal case the argument is similar. Suppose that v is a strongly generating world in $\mathfrak {M}^{S'}$ and that $\lnot (vR^{S'}_\square v)$ and $\lnot (vR^{S'}_\blacksquare v)$. Then, for some formulas $\psi$ and $\chi$, we have $\square \psi ,\blacksquare \chi ,\lnot \psi ,\lnot \chi \in v$. From this we can infer that $\psi \vee \chi \in u$ for every world u s.t. $u\ne v$ and so that v is the unique world in $\mathfrak {M}^{S'}$ s.t. $\lnot (\psi \vee \chi )\in v$. Again, this cannot be the case, since, for every propositional variable p not in $\psi \vee \chi$, both sets $\{\lnot (\psi \vee \chi ), p\}$ and $\{\lnot (\psi \vee \chi ), \lnot p\}$ are $S'$-consistent and so they can be extended to two maximally $S'$-consistent sets of formulas corresponding to two different worlds in $\mathfrak {M}^{S'}$. The rest follows as in the monomodal case. $\square$

Proposition 3.4

A consistent normal monomodal (bimodal) system S is closed under $RDis_\square$ ($RDis_{\square \blacksquare }$) iff the canonical model of S is strongly generated.

Proof

Theorem 6.5 in Hughes and Cresswell (1984) and Proposition 3.2 above provide the left-to-right direction of the biconditional. For the right-to-left direction it is sufficient to notice that if w is a strongly generating world of a system S and $\vdash _S\square \phi _1\vee ...\vee \square \phi _n$ (in the bimodal case, $\vdash _S (\square \phi _1\wedge \blacksquare \phi _1)\vee ...\vee (\square \phi _n\wedge \blacksquare \phi _n)$), then $\square \phi _1\vee ...\vee \square \phi _n\in w$ ($(\square \phi _1\wedge \blacksquare \phi _1)\vee ...\vee (\square \phi _n\wedge \blacksquare \phi _n)\in w$) and we have $\square \phi _i\in w$ ($\square \phi _i\wedge \blacksquare \phi _i\in w$) for some i s.t. $1\le i \le n$. Therefore, by the properties of strongly generating worlds and Proposition 3.3, $\phi _i\in v$ for all $v\in W^S$, whence $\phi _i\in Th(S)$. This means that S is closed under $RDis_\square$ ($RDis_{\square \blacksquare }$). $\square$

On the other hand, Hughes and Cresswell’s strategy based on strongly generating worlds cannot be applied to systems closed under any of the following schemata:

$B_\square$:

$\phi \rightarrow \square \lozenge \phi$;

$5_\square$:

$\lozenge \phi \rightarrow \square \lozenge \phi$.

Indeed, suppose that the canonical model of a system S closed under $B_\square$ included a strongly generating world w; then, for every propositional variable p we would have either (I) $p\in w$ or (II) $\lnot p\in w$. Even if w had no access to itself, it would have certainly access to some world u s.t. $p\in u$ and to some world $u'$ s.t. $\lnot p \in u'$; therefore, we could infer $\lozenge p,\lozenge \lnot p\in w$. Furthermore, since the canonical model of a system closed under $B_\square$ is built over a symmetric frame, then, for every world $v\in W^S$ s.t. $v\ne w$, we would have $v R_\square w$. Thus, in case (I) we would get $\lozenge p\in z$ for all $z\in W^S$ and so $\lozenge p\in Th(S)$, while in case (II) we would get $\lozenge \lnot p\in z$ for all $z\in W^S$ and so $\lozenge \lnot p\in Th(S)$. A contradiction would result in both cases, since no consistent normal monomodal system has either $\lozenge p$ or $\lozenge \lnot p$ among its theorems.

Similarly, suppose that the canonical model of a system $S'$ closed under $5_\square$ included a strongly generating world w; then, for any $p\in VAR$ there would be a world u s.t. $wR_\square u$ and $p\in u$; therefore, we would have $\lozenge p,\square \lozenge p\in w$ and $\lozenge p\in Th(S')$, which is, again, impossible.

Finally, one can rely on $RDis_\square$ to obtain additional negative results on the existence of strongly generating worlds. For instance, Hughes and Cresswell (1984, p. 78) observe that no extension of $\mathbf{S4.2 }_\square$ is closed under $RDis_\square$, where $\mathbf{S4.2 }_\square$ is the system obtained by extending the axiomatic basis of ${\mathbf{S4}}_\square$ with the principle below:

$G1_\square$:

$\lozenge \square \phi \rightarrow \square \lozenge \phi$.

Indeed, if S is an extension of $\mathbf{S4.2 }_\square$, then $\square \lozenge p\vee \square \lozenge \lnot p\in Th(S)$ for any $p\in VAR$, while $\lozenge p, \lozenge \lnot p\notin Th(S)$. This means that $RDis_\square$ fails in S and so, in the light of Proposition 3.4, that the canonical model of S is not strongly generated.

4 The Method of Isolated Worlds

Showing that the canonical model of a system S does not include any strongly generating world is not sufficient to claim that the model is non-cohesive; indeed, in such case it is still possible that all pairs of different states in the domain are related by a pseudo-accessibility walk. For instance, a monomodal frame with three states $w_1$, $w_2$ and $w_3$ s.t. $R_\square =\{(w_1,w_2),(w_3,w_2)\}$ is not strongly generated but cohesive. Furthermore, Hughes and Cresswell exploit $RDis_\square$ only to show that the canonical model of a system closed under it includes a strongly generating world. We will see below that this rule (as well as its bimodal analogue introduced in Sect. 3) can be also used to prove non-cohesiveness in the case of specific systems; however, here we are interested in finding general properties that guarantee the non-cohesiveness of the canonical model for a possibly large class of systems. To this aim, we look for a strategy able to point out directly the presence of at least two worlds not related by any pseudo-accessibility walk in the frame of the canonical model.

The strategy adopted in this Section can be described as follows. Suppose that a monomodal frame includes a state w s.t. (I) $R_\square (w)-\{w\}=\emptyset$ and (II) $w\notin R_\square (v)$ for any $v\ne w$: then there is no pseudo-accessibility walk between w and any other (distinct) state in the domain. Similarly, suppose that a bimodal frame includes a state w s.t. (I) $(R_\square (w)\cup R_\blacksquare (w))-\{w\}=\emptyset$ and (II) $w\notin R_\square (v)\cup R_\blacksquare (v)$ for any $v\ne w$: then there is no pseudo-accessibility walk between w and any other (distinct) state in the domain. Thus, in order to claim that a frame is not cohesive it is sufficient to show that it includes a state w with these properties, which can be called an isolated world. In what follows we will prove that the canonical frame of relevant classes of monomodal and bimodal systems includes some isolated worlds.

Let S and $S'$ be two consistent normal modal systems s.t. $S'$ is an extension of S. Since $Th(S)\subseteq Th(S')$ and $\bot \notin Th(S')$, then the canonical model of S, $\mathfrak {M}^S$, includes some state w s.t. $Th(S')\subseteq w$; such a state can be called an $S'$-consistent state in $\mathfrak {M}^S$. Relying on this fact, we illustrate below which are the degenerate clusters and the simple clusters in the canonical model of a system.

Proposition 4.1

In the canonical model of any normal monomodal (bimodal) system S the set of $\mathbf{Ver }_\square$-consistent ($\mathbf{Ver }_{\square \blacksquare }$-consistent) worlds is the set of degenerate clusters and the set of $\mathbf{Triv }_\square$-consistent ($\mathbf{Triv }_{\square \blacksquare }$-consistent) worlds is the set of simple clusters.

Proof

Consider degenerate clusters in the monomodal case. Any $\mathbf{Ver }_\square$-consistent state w in $\mathfrak {M}^S$ is clearly a degenerate cluster, since $\square \bot \in w$ and $\bot$ does not belong to any maximal consistent set of formulas. Conversely, if w is not a $\mathbf{Ver }_\square$-consistent state, then there is some formula $\sigma$ s.t. $\lnot \square \sigma \in w$. From this it follows that the set $\square ^-(w)\cup \{\lnot \sigma \}$ is S-consistent and contained in some u in $W^S$. Indeed, otherwise we would have $\vdash _S (\phi _1\wedge ...\wedge \phi _n)\rightarrow \sigma$ for some $\phi _1,...,\phi _n\in \square ^-(w)$ and, by ordinary modal reasoning, we would get $\vdash _S (\square \phi _1\wedge ...\wedge \square \phi _n)\rightarrow \square \sigma$, so $\square \sigma \in w$: contradiction. Since, by definition, $w R^S_\square u$, then w is not a degenerate cluster. A similar argument can be used in a bimodal setting with reference to $\mathbf{Ver }_{\square \blacksquare }$-consistent worlds: one direction is trivial, while the relevant difference in the converse direction is that the claim that $\lnot \square \sigma \in u$ has to be replaced with the weaker claim that $\lnot \square \sigma \vee \lnot \blacksquare \sigma \in u$ and the rest has to be changed accordingly.

Consider simple clusters in the monomodal case. Any $\mathbf{Triv }_\square$-consistent world w is clearly a simple cluster, since $\square ^-(w)\subseteq w$, so $w R^S_\square w$, and for any $u\ne w$ there is $\sigma \in \mathcal {L}_\square$ s.t. $\sigma \in w$ and $\sigma \notin u$, so $\square \sigma \in w$ and $\square ^-(w)\nsubseteq u$, whence $\lnot (w R^S_\square u)$. Conversely, for any world u which is not $\mathbf{Triv }_\square$-consistent there is some $\tau \in \mathcal {L}_\square$ s.t. either $\lnot \tau ,\square \tau \in u$ or $\tau ,\lnot \square \tau \in u$. In the first case, since $\square ^-(u)\nsubseteq u$, then $\lnot (u R^S_\square u)$ and u is not a simple cluster. In the second case, the set $\square ^-(u)\cup \{\lnot \tau \}$ is S-consistent and contained in some $v\in W^S$, for reasons illustrated above; of course, $v\ne u$ and this means that u is not a simple cluster. A similar argument can be used in a bimodal setting with reference to $\mathbf{Triv }_{\square \blacksquare }$-consistent worlds: also in this case one direction is trivial, while the relevant difference in the converse direction is that the claim that either $\lnot \tau ,\square \tau \in u$ or $\tau ,\lnot \square \tau \in u$ has to be replaced with the weaker claim that either $\lnot \tau ,\square \tau \vee \blacksquare \tau \in u$ or $\tau ,\lnot \square \tau \vee \lnot \blacksquare \tau \in u$ and the rest has to be changed accordingly. $\square$

Proposition 4.1 points out a peculiar aspect of canonical models. Indeed, focusing on the relation between Th(Triv$_{\square })$ and simple clusters in canonical models for monomodal systems, we could rephrase the corresponding part of Proposition 4.1 as follows: for any $w\in W^S$, w is a simple cluster iff $\mathfrak {M}^S,w\vDash \phi$ whenever $\phi \in Th($Triv$_{\square })$. On the other hand, this is not the case, in general, for ordinary models, since we can have all theorems of Triv$_{\square }$ true at a state u of a non-canonical model $\mathfrak {M}$ without u being a simple cluster. In what follows we show that in the canonical models of some classes of normal monomodal and bimodal systems simple clusters and degenerate clusters are also isolated worlds and this is sufficient to claim that such canonical models are non-cohesive.

We denote by $!^n$ a string of length n, for some $n\ge 0$, composed by the operators $\square$ and $\lozenge$. Given that $\square$ and $\lozenge$ are interdefinable, $!^n$ can be called a monomodal sequence.

Proposition 4.2

Any normal monomodal system S which has one of the following properties has a non-cohesive canonical model:

P1:

S is contained in $\mathbf{Ver }_\square$ and $\vdash _S\square \lozenge \top$;

P2:

S is contained in $\mathbf{Triv }_\square$ and, for some $n\ge 0$, $\vdash _S\phi \rightarrow \square \bigvee _{0\le i\le n}!^i\phi$.⁷

Proof

Let S be a system satisfying property P1. Then, the canonical model of S includes some $\mathbf{Ver }_\square$-consistent world w. Let v be an arbitrary world in $W^S$ s.t. $v\ne w$; then, by P1, $\square \lozenge \top \in v$. This means that $\lozenge \top \in u$ for every $u\in R^S_\square (v)$. However, since w is a $\mathbf{Ver }_\square$-consistent world, then $\lozenge \top \notin w$; therefore, $w\notin R^S_\square (v)$. Notice that v is an arbitrary world in $W^S$ s.t. $v\ne w$, so w is not accessible from any other world in the domain. Moreover, Proposition 4.1 tells us that w is a degenerate cluster. Thus, we can conclude that w is an isolated world.

Let S be a system satisfying property P2. Then, the canonical model of S includes some world w which is ${\mathbf{Triv}}_\square$-consistent. Let v be an arbitrary world in $W^{S}$ s.t. $v\ne w$. Then, there is some $\psi \in \mathcal {L}_\square$ s.t. $\psi \in v$ and $\psi \notin w$. From P2 it follows that there is some $n\ge 0$ s.t. $\square \bigvee _{0\le i\le n} !^i\psi \in v$ and this, in turn, means that $\bigvee _{0\le i\le n} !^i\psi \in u$ for any $u\in R^{S}_\square (v)$. However, since w is a ${\mathbf{Triv}}_\square$-consistent world and $\vdash _{\mathbf{Triv}_\square }!^k\psi \equiv \psi$ for any $k\ge 0$, then $\bigvee _{0\le i\le n} !^i\psi \in w$ iff $\psi \in w$, hence $w\notin R^{S}_\square (v)$. This means that w is not accessible from any other (distinct) world in the domain. Moreover, Proposition 4.1 tells us that w is a simple cluster; thus, we can conclude that it is an isolated world. $\square$

   We now illustrate some consequences of Proposition 4.2. All normal monomodal systems between $\mathbf{K5}_\square$ ($=$$\mathbf{K }_\square + \{5_\square \}$) and $\mathbf{Ver }_\square$ satisfy P1, due to the fact that $\vdash _\mathbf{K5 _\square }\square \lozenge \top$; thus, they all have a non-cohesive canonical model. Furthermore, all normal consistent extensions of $\mathbf{KB }_\square$ ($=$$\mathbf{K }_\square$$+ \{B_\square \}$) satisfy either P1 or P2, due to the fact that $\vdash _\mathbf{KB _\square }\phi \rightarrow \square \lozenge \phi$ and $\vdash _\mathbf{KB _\square }\square \lozenge \top$; thus, their canonical models are non-cohesive as well. Notice also that according to the proof of Proposition 4.2 (where w is always taken to represent either an arbitrary degenerate cluster or an arbitrary simple cluster), any normal monomodal system satisfying both P1 and P2, like $\mathbf{KB }_\square$ and its extension $\mathbf{KTc }_\square$ ($= \mathbf{K }_\square + \{Tc_\square \}$), has a canonical model in which all degenerate clusters and all simple clusters are isolated worlds.

In general, if $|VAR|=k$, then whenever the canonical model of a normal monomodal system includes a $\mathbf{Ver }_\square$-consistent world or a $\mathbf{Triv}_\square$-consistent world, it includes $2^k$ worlds of the same kind (resulting from a different valuation of propositional variables); this means that if VAR is countably infinite, then any monomodal system satisfying a property among P1 and P2 has a canonical model with uncountably many isolated worlds. The extreme cases are the canonical models of $\mathbf{Ver }_\square$, $\mathbf{Triv}_\square$ and $\mathbf{KTc }_\square$, in which all worlds are isolated, since the first one includes only degenerate clusters, the second one only simple clusters and the third one only degenerate or simple clusters.

We know that a normal monomodal system is closed under $RDis_\square$ iff its canonical model is strongly generated (Proposition 3.4). Thus, all systems which satisfy some property among P1 and P2 cannot be closed under $RDis_\square$. In some cases it is easy to find system-specific counterexamples to $RDis_\square$. For instance, K5$_\square$ has among its theorems $\square p\vee \square \lozenge \lnot p$; however, neither p nor $\lozenge \lnot p$ is provable in such system. In a more systematic perspective, it is interesting to notice that P1 and P2 provide some general counterexamples to $RDis_\square$. Indeed, if a system S satisfies P1, then $\vdash _S\square \lozenge \top$ and $Th(S)\subseteq Th(\mathbf Ver _{\square })$, so $\nvdash _S\lozenge \top$, which is enough for the failure of $RDis_\square$. Furthermore, if a system $S'$ satisfies P2, then $\vdash _{S'}\lozenge p\rightarrow \square \bigvee _{0\le i \le n} !^i\lozenge p$, that is $\vdash _{S'}\square \lnot p\vee \square \bigvee _{0\le i \le n} !^i\lozenge p$. We know that $\nvdash _S \lnot p$ for any consistent normal system S; furthermore, since $Th(S')\subseteq Th(\mathbf Triv _{\square })$, then $\vdash _{S'}\bigvee _{0\le i \le n} !^i\lozenge p$ would entail $\vdash _\mathbf{Triv _\square }\bigvee _{0\le i \le n} !^i\lozenge p$; however we know that $\vdash _\mathbf{Triv _\square }\bigvee _{0\le i \le n} !^i\lozenge p$ iff $\vdash _\mathbf{Triv _\square }p$ and the latter is clearly not the case. Thus $RDis_\square$ fails in $S'$.

Moreover, one can sometimes combine the existence of $\mathbf{Ver }_\square$-consistent worlds or $\mathbf{Triv }_\square$-consistent worlds in the canonical model of a system with the failure of $RDis_\square$ in order to get an alternative proof of non-cohesiveness. For instance, in the case of $\mathbf{KB }_\square$, we have that $\vdash _\mathbf{KB _\square }\square \lozenge p\vee \square \lozenge \lnot p$, while $\lozenge p,\lozenge \lnot p\notin Th(\mathbf KB _\square )$. Not only this, but the set $\{\lnot \lozenge p,\lnot \lozenge \lnot p\}$ is $\mathbf{KB }_\square$-consistent, being a subset of every $\mathbf{Ver }_\square$-consistent world in the canonical model of $\mathbf{KB }_\square$ (and we know that there are some). Thus, all such worlds cannot be accessible from any others and they are degenerate clusters, due to Proposition 4.1; therefore, they are isolated worlds. However, this procedure is system-specific; for instance, the same example would not work for KTB$_\square$, since $\{\lnot \lozenge p,\lnot \lozenge \lnot p\}$ is not a KTB$_\square$-consistent set.

Now we will illustrate how the method of isolated worlds can be put at work in a bimodal context. Let M and $M'$ stand for an arbitrary operator between $\lozenge$ and $\blacklozenge$ and L and $L'$ for an arbitrary operator between $\square$ and $\blacksquare$. Furthermore, let $?^n$ stand for a string of length n, for some $n\ge 0$, composed by the operators $\square$, $\blacksquare$, $\lozenge$ and $\blacklozenge$; we will say that $?^n$ denotes a bimodal sequence.

Proposition 4.3

Any normal bimodal system S which has one of the following properties has a non-cohesive canonical model:

P3:

S is contained in Ver$_{\square \blacksquare }$ and $\vdash _S\square M\top \wedge \blacksquare M'\top$.

P4:

S is contained in $\mathbf{Triv }_{\square \blacksquare }$ and $\vdash _S\phi \rightarrow (\square \bigvee _{0\le i\le n} ?^i\phi \wedge \blacksquare \bigvee _{0\le j\le l} ?^j\phi )$, for some $n,l\ge 0$.

Proof

Let S be a bimodal system satisfying property P3. Then the canonical model of S includes some $\mathbf{Ver }_{\square \blacksquare }$-consistent world w. Let v be an arbitrary world in $W^S$ s.t. $v\ne w$; then, by P3, $\square M\top \wedge \blacksquare M'\top \in v$. From this one can infer that $M\top \in u$ for every $u\in R^S_\square (v)$ and $M'\top \in z$ for every $z\in R^S_\blacksquare (v)$. However, since w is a $\mathbf{Ver }_{\square \blacksquare }$-consistent world, then $\lozenge \top \notin w$ and $\blacklozenge \top \notin w$. Therefore, $w\notin R^S_\square (v)\cup R^S_\blacksquare (v)$. Since v is an arbitrary world s.t. $v\ne w$, then w is not accessible from any other world in the domain. Furthermore, Proposition 4.1 tells us that w is a degenerate cluster; thus, we can conclude that w is an isolated world.

Let S be a bimodal system satisfying property P4. Then, the canonical model of S includes some Triv$_{\square \blacksquare }$-consistent world w. Let v be an arbitrary world in $W^{S}$ s.t. $v\ne w$. Then, there is some $\psi \in \mathcal {L}_{\square \blacksquare }$ s.t. $\psi \in v$ and $\psi \notin w$. By P4, $\square \bigvee _{0\le i\le n} ?^i\psi \wedge \blacksquare \bigvee _{0\le j\le l} ?^j\psi \in v$ for some $n,l\ge 0$. From this one can infer that $\bigvee _{0\le i\le n} ?^i\psi \in u$ for any $u\in R^{S}_\square (v)$ and that $\bigvee _{0\le j\le l} ?^j\psi \in t$ for any $t\in R^{S}_\blacksquare (v)$. Since w is a Triv$_{\square \blacksquare }$-consistent world, then $?^k\psi \in w$ iff $\psi \in w$ for any $k\ge 0$; hence $w\notin R^{S}_\square (v)\cup R^{S}_\blacksquare (v)$ for any $v\ne w$. Furthermore, Proposition 4.1 tells us that w is a simple cluster; thus, we can conclude that it is also an isolated world. $\square$

The duplication of any monomodal system satisfying property P1 or P2 clearly satisfies P3 or P4. More generally, a system with a separable axiomatic basis $S\otimes S'$ has property P3 whenever both S and $S'$ satisfy P1 and has property P4 whenever both S and $S'$ satisfy P2. On the other hand, since it is not always the case that a normal bimodal system is contained either in $\mathbf{Ver }_{\square \blacksquare }$ or in $\mathbf{Triv }_{\square \blacksquare }$,⁸ we provide here syntactical criteria which are sufficient for this to be the case, before illustrating other consequences of Proposition 4.3.

Given a formula $\phi \in \mathcal {L}_{\square \blacksquare }$, let us say that a maximal modal subformula of $\phi$ is any subformula of $\phi$ of kind $\square \psi$ or $\blacksquare \psi$ which is not in the scope of a modal operator. For instance, the maximal modal subformulas of $(\square (\blacksquare p\vee \square \blacksquare \blacksquare q) \wedge \square r)\equiv q$ are $\square (\blacksquare p\vee \square \blacksquare \blacksquare q)$ and $\square r$.

Proposition 4.4

Any consistent and normal bimodal system S s.t. for every formula $\phi \in Th(S)$, we also have $\phi ^*\in Th(S)$, where $\phi ^*$ is obtained from $\phi$ by replacing all maximal modal subformulas with $\top$, is contained in ${\mathbf{Ver}}_{\square \blacksquare }$. Furthermore, any consistent and normal bimodal system $S'$ s.t. for every formula $\phi \in Th(S')$, we also have $\phi ^{**}\in Th(S')$, where $\phi ^{**}$ is obtained from $\phi$ by removing all occurrences of $\square$ and $\blacksquare$, is contained in ${\mathbf{Triv}}_{\square \blacksquare }$.

Proof

Let S be a consistent and normal extension of ${\mathbf{K}}_{\square \blacksquare }$ such that for every $\phi \in Th(S)$, $\phi ^*\in Th(S)$; suppose that there is some formula $\psi$ s.t. $\psi \in Th(S)$ while $\psi \notin Th({\mathbf{Ver}}_{\square \blacksquare })$. Notice that all normal modal systems are closed under replacement of provable equivalents; thus, since, for any formula $\chi$, $(\square \chi \equiv \top )\wedge (\blacksquare \chi \equiv \top )\in Th({\mathbf{Ver}}_{\square \blacksquare })$, we have $\psi \notin Th({\mathbf{Ver}}_{\square \blacksquare })$ iff $\psi ^*\notin Th({\mathbf{Ver}}_{\square \blacksquare })$. By definition, $\psi ^*$ is a formula including no modal operator and we must have $\psi ^*\notin Th({\mathbf{PC}})$, since $Th({\mathbf{PC}})\subseteq Th({\mathbf{Ver}}_{\square \blacksquare })$. However, since PC is a Post-complete system, then no consistent extension of it can have $\psi ^*$ as a theorem, hence $\psi \notin Th(S)$: contradiction.

Let $S'$ be a consistent and normal extension of K$_{\square \blacksquare }$ such that for every $\phi \in Th(S')$, $\phi ^{**}\in Th(S')$; suppose that there is some formula $\psi$ s.t. $\psi \in Th(S')$ while $\psi \notin Th({\mathbf{Triv}}_{\square \blacksquare })$. Since, for any formula $\chi$, $(\square \chi \equiv \chi )\wedge (\blacksquare \chi \equiv \chi )\in Th({\mathbf{Triv}}_{\square \blacksquare })$, we have $\psi \notin Th({\mathbf{Triv}}_{\square \blacksquare })$ iff $\psi ^{**}\notin Th({\mathbf{Triv}}_{\square \blacksquare })$. By definition, $\psi ^{**}$ is a formula including no modal operator and the rest of the argument runs as in the previous case. $\square$

   All normal systems of tense logic satisfying one of the conditions mentioned in Proposition 4.4 have a non-cohesive canonical model, since they also satisfy either P3 or P4, due to the fact that $\vdash _\mathbf{K _t} \square \blacklozenge \top \wedge \blacksquare \lozenge \top$ and $\vdash _\mathbf{K _t} \phi \rightarrow \square \blacklozenge \phi \wedge \blacksquare \lozenge \phi$. The properties P3 and P4 are clearly satisfied also by some normal systems of bimodal logic that are not closed under RMI, such as $\mathbf{KTc }_\square \otimes \mathbf{KB }_\blacksquare$ or $\mathbf{K }_b$. Furthermore, any normal bimodal system satisfying both P3 and P4, like K$_t$ or KTc$_{\square \blacksquare }$, has a canonical model in which all degenerate clusters and all simple clusters are isolated worlds. Relying on the same argument used in the monomodal case, we can claim that if $|VAR|=k$, then any normal bimodal system satisfying a property among P3 and P4 has a canonical model including $2^k$ isolated worlds.

Actually, in the case of systems of tense logic it is possible to provide a very general result of non-cohesiveness, that does not rely on the method of isolated worlds and was pointed out by an anonymous referee of the present article. We illustrate such result in Proposition 4.5.

Proposition 4.5

The canonical model of every normal system of tense logic is non-cohesive.

Proof

Let S be a normal and consistent system of tense logic. It can be proved that, for every $p\in VAR$, the canonical model of S includes a state w s.t. $\{L^np:n\in \mathbb {N}\}\subseteq w$. Indeed, suppose that this is not the case; then, there is some $k\ge 0$ s.t. $\vdash _S\lnot \bigwedge _{0\le i\le k}L^ip$. Since S is closed under uniform substitution, then $\vdash _S\lnot \bigwedge _{0\le i\le k}L^i\top$. However, given that S is closed under $RN_\square$ and $RN_\blacksquare$, then $\vdash _S L^j\top$ for every $j\in \mathbb {N}$ and so $\vdash _S \bigwedge _{0\le i\le k}L^i\top$: contradiction. Therefore, $\{L^np:n\in \mathbb {N}\}$ can be extended to a maximally S-consistent set of formulas w. As a consequence, for every $n\in \mathbb {N}$, $\lnot M^n \lnot p\in w$. The canonical model of S obviously includes some state v s.t. $\lnot p\in v$. Since $R_\square$ and $R_\blacksquare$ are reciprocally converse in the frame of the canonical model of S (due to BR1 and BR2, as discussed in Sect. 2), then there cannot be any pseudo-accessibility walk between w and v. Indeed, suppose that there were a sequence of states $(w_0,...,w_l)\in W^{S^{l+1}}$ s.t. $w_0=w$, $w_l=v$ and for each $i<l$ either $w_i R_\square w_{i+1}$ or $w_{i+1} R_\square w_{i}$ or $w_i R_\blacksquare w_{i+1}$ or $w_{i+1} R_\blacksquare w_{i}$; then $M^l\lnot p\in w$, for some sequence of possibility operators $M^l$, which would lead to a contradiction. $\square$

5 Final Comments

In this article we explored the issue of cohesiveness in canonical models by extending some preliminary results obtained by Hughes and Cresswell. Beside showing how their methods involving $RDis_\square$ or a strongly generating world can lead to new system-specific results and can be exploited in a bimodal setting, we introduced the method of isolated worlds, which allows one to claim that the canonical model of a quite large class of normal monomodal and bimodal systems is based on a non-cohesive frame. In Table 1 we summarize some of the most relevant results obtained.

Table 1 Cohesivenss in canonical models

During the exposition, we presented some problems that remained open, for instance whether the canonical model of normal extensions of $\mathbf{S4.2 }_\square$ or the one of systems between $\mathbf{K5 }_\square$ and $\mathbf{Triv }_\square$ is cohesive; in the light of what is said in Sect. 3, one would be inclined to think that the answer to this question is negative. However, the method of isolated worlds does not seem to work to settle these cases. The possibility of generalizing the methods discussed here to deal with multimodal languages including an arbitrary number of primitive operators of necessity represents another important direction for future investigations in this area.

Finally, it would be interesting to check whether non-cohesiveness is a monotonic property, in the sense that if a system S has a non-cohesive canonical model and $S'$ is an extension of S, then $S'$ has a non-cohesive canonical model as well. The results available so far seem to suggest that this is the case. On the one hand, this would contrast with the fact, observed in Hughes and Cresswell (1984), that closure under $RDis_\square$ is not a monotonic property, since the system $\mathbf{K }_\square + \{\square (\square \phi \rightarrow \phi )\vee \square (\square \phi \rightarrow \square \square \phi )\}$ provides counterexamples to $RDis_\square$, despite being between $\mathbf{K }_\square$ and $\mathbf{KT }_\square$, which are both closed under such rule. On the other hand, we know by Proposition 3.4 that the failure of $RDis_\square$ is not sufficient to prove non-cohesiveness (being equivalent to the claim that the canonical model does not include any strongly generating world), so such a discrepancy with respect to monotonicity would not represent an issue.