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):
Furthermore, we will say that a world
w is a
simple cluster iff:
Accessibility relations can be used to define
accessibility walks in frames.
For the aims of the present article it is fundamental to introduce also the notion of a pseudo-accessibility walk.
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.
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 \)).
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.
2 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.
3 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\).
4 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:
\(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,
5 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):
6It 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:
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\).
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.
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 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.
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.
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 }\),
8 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\).
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.