Proof. Since $\mathbf {S4}\subseteq \boldsymbol {\Lambda }$ and $\mathbf {Q}\boldsymbol {\Lambda }$ is Kripke complete, it follows, by [Reference Ghilardi3, Theorem 7.3], that either $\boldsymbol {\Lambda } \subseteq \mathbf {S4.3}$ or $\mathbf {S5}\subseteq \boldsymbol {\Lambda }$ . Since $\mathbf {S4.3}$ is not locally tabular, and local tabularity is preserved for extensions, surely $\boldsymbol {\Lambda }\not \subseteq \mathbf { S4.3}$ . Hence, $\mathbf {S5}\subseteq \boldsymbol {\Lambda }$ .

Proof. By Segerberg’s theorem [Reference Chagrov and Zakharyaschev1, Theorem 12.21], $\mathbf {S4Alt}_n$ is locally tabularFootnote ⁹ Since $\textbf {S5}$ is refuted on a two-element chain, which validates $\mathbf {S4Alt}_n$ , surely $\textbf {S5} \not \subseteq \mathbf {S4Alt}_n$ . Hence, by Theorem 4.1, $\mathbf {QS4Alt}_n$ is Kripke incomplete.

Proof. Fix $n \geqslant 1$ and suppose that $\boldsymbol {F} = (W, R, D)$ is a $\mathbf {QK4Alt}_n$ -frame. By Proposition 2.4, $(W, R) \models \mathbf {K4Alt}_n$ , and so, by Proposition 2.2(1) and (3), R is transitive and $|R(u)| \leqslant n$ , for every $u \in W$ . To prove that $\boldsymbol {F} \models A_n$ , we assume that $\boldsymbol {F}, u_0 \models \Diamond ^{n+1} \top $ to show that $\boldsymbol {F}, u_0 \models \Diamond \forall \mathit {ref}$ , for an arbitrary $u_0$ from $\boldsymbol {F}$ . Since $\boldsymbol {F}, u_0 \models \Diamond ^{n+1} \top $ , there exist $u_1, \ldots , u_{n+1} \in W$ such that $u_0 R u_1 \ldots u_n R u_{n+1}$ ; hence, by transitivity, $u_0Ru_i$ , for every $i \in \{1, \ldots , n+1\}$ . Since $|R(u_0)| \leqslant n$ , there exist $i, j \in \{1, \ldots , n+1\}$ such that $i\neq j$ and $u_{i} = u_j$ . Since R is transitive, it follows that $u_i$ is reflexive. Hence, $\boldsymbol {M},u_i \models \square P(a) \rightarrow P(a)$ , for every model $\boldsymbol {M}$ over $\boldsymbol {F}$ and every $a\in D_{u_i}$ . Thus, $\boldsymbol {F}, u_i \models \forall \mathit {ref}$ , and so $\boldsymbol {F}, u_0 \models \Diamond \forall \mathit {ref}$ .

Proof. In view of Proposition 4.3, it suffices to obtain a Kripke bundle strongly validating $\mathbf {SL4}$ , but not $A_n$ . To that end, we use a Kripke bundle from [Reference Shehtman7] (see Figure 1):

$$ \begin{align*}\begin{array}{ccccl}\!\!\! W := \{ u \}, &\!\! R := \{ (u, u) \}, &\!\! D_u := \{a, b \}, &\!\! \rho_{u u} := \{(a, b), (b, b) \},&\!\! \mathbb{F}_0 := (W, R, D, \rho). \end{array} \end{align*} $$

Figure 1

Kripke bundle $\mathbb {F}_0$ .

To see that $\mathbb {F}_0 \not \models ^+ A_n$ , consider the model $\mathbb {M}_b = (\mathbb {F}_0, \xi )$ where $\xi _u(P) = \{ b \}$ . Since $R(u)=\{u\}$ , $\rho _{uu}(a)=\{b\}$ , and $\mathbb {M}_b, u \models P(b)$ , it follows that ${\mathbb {M}_b, u \models \square P(a)}$ . Since also $\mathbb {M}_b, u \not \models P(a)$ , it follows that $\mathbb {M}_b, u \not \models \square P(a) \to P(a)$ and so $\mathbb {M}_b, u \not \models \forall \mathit {ref}$ . Since u sees only itself, $\mathbb {M}_b, u \not \models \Diamond \forall \mathit {ref}$ . On the other hand, since R is serial, $\mathbb {M}_b, u \models \Diamond ^{n+1} \top $ . Hence, $\mathbb {M}_b, u \not \models A_n$ , and so $\mathbb {F}_0 \not \models ^+ A_n$ .

That $\mathbb {F}_0 \models ^+ \mathbf {SL4}$ was observed in [Reference Shehtman7, Proof of Lemma 5.12]: by Proposition 4.5, it suffices to check that, for every propositional frame $F_k = (D_k, R_k)$ associated with $\mathbb {F}_0$ (see Definition 4.4), $F_k \models \mathbf {SL4}$ ; this holds since every $R_k$ is transitive and functional (and, hence, $1$ -alternative).

Proof. Let L be a logic such that $\mathbf {QK4Alt}_n \subseteq L \subseteq \mathbf {QSL4}$ . By Lemma 4.6, $L \models _{\mathcal {K}} A_n$ , and, by Lemma 4.7, $L \not \vdash A_n$ . The statement of the theorem follows.

Proof. Suppose that $\boldsymbol {F} =(W,R,D)$ is a $\mathbf {QK4.1}$ -frame, and so, by Proposition 2.4, $(W,R)\models \mathbf {K4.1}$ . Then, by Propositions 2.2(3) and 2.3, R is transitive and every world from W sees a maximal world.

To prove that $\boldsymbol {F} \models B_1$ , we consider a model over $\boldsymbol {F}$ and, assuming that, in that model, $u \models \Diamond \square \exists x P(x)$ , show that $u \models \Diamond \exists x\square P(x)$ . Since $u \models \Diamond \square \exists x P(x)$ , there exists ${v \in R(u)}$ such that $v \models \square \exists x P(x)$ . Let w be a maximal world accessible from $v$ . Then, $w \models \exists x P(x)$ , and so $w \models P(a)$ , for some $a \in D_w$ . Since w is maximal, surely $w \models \square P(a)$ , and so $w \models \exists x \square P(x)$ . Since R is transitive, $w \in R(u)$ ; hence, $u \models \Diamond \exists x\square P(x)$ .

Proof. First, we recall that $\mathbf {K}+\boldsymbol {ma}\vdash \Diamond \top $ : since $\mathbf {K}\vdash \square \top $ , it follows that $\mathbf {K}+\square \Diamond \top \rightarrow \Diamond \square \top \vdash \square \Diamond \top \rightarrow \Diamond \top $ ; since $\mathbf {K}\vdash \square \bot \rightarrow \square \Diamond \top $ , it then follows that $\mathbf {K}+\boldsymbol {ma}\vdash \square \bot \rightarrow \Diamond \top $ , and so $\mathbf {K}+\boldsymbol {ma}\vdash \Diamond \top $ . Thus, every Kripke frame validating $\boldsymbol {\Lambda }$ is serial.

By assumption, there exists a Kripke frame F such that $\boldsymbol {\Lambda }={\textbf {L}}(F)$ . As we have seen, F is serial; moreover, since $\boldsymbol {\Lambda } \ne \mathbf {Triv}$ , this frame is not a singleton. Hence, there exists a nontrivial rooted generated subframe $G = (W, R)$ of F, and so, by Generation lemma (the propositional version of Proposition 2.8(2)), $\boldsymbol {\Lambda }={\textbf {L}}(F)\subseteq {\textbf {L}}(G)$ .

Now, consider Kripke frames (see Figure 2)

$$ \begin{align*}\begin{array}{lcl} G_1:=(\{a,b\},\{(a,b),(b,b)\}) & ~\text{and}~ & G_2:=(\{c,d\},\{(c,c),(c,d),(d,d)\}). \end{array} \end{align*} $$

One can show, using standard modal logic arguments, that ${\textbf {L}}(G_1) = \mathbf {SL4}$ and ${\textbf {L}}(G_2) = \mathbf {S4.1Alt}_2$ . (The simplest way is to use Bellissima’s completeness theorem mentioned in the introduction and consider rooted frames validating these logics: there are only a few possibilities.)

Figure 2

Kripke frames $G_1$ (left) and $G_2$ (right).

Figure 2. Long description

The figure consists of two separate directed graphs.

In the left panel, G 1, there are two nodes labeled a and b. A horizontal arrow points from node a on the left to node b on the right. Node b has a circular arrow representing a self-loop.

In the right panel, G 2, there are two nodes labeled c and d. Node c on the left has a circular arrow representing a self-loop. A horizontal arrow points from node c to node d on the right. Node d also has a circular arrow representing a self-loop.

Next, we show that either $G \twoheadrightarrow G_1$ or $G\twoheadrightarrow G_2$ .

Let $u_0$ be the root of G (thus, $W = \{u_0\} \cup R(u_0)$ ) and $C_0$ be the cluster of G containing $u_0$ . Since G is nontrivial and $G \models \boldsymbol {ma}$ , it follows, by Proposition 2.3, that G is not a cluster; hence, $C_0 \neq W$ . Now, if $u_0$ is irreflexive, then there exists a p-morphism of G onto $G_1$ sending $u_0$ to a, and all other points to b. If, on the other hand, $u_0$ is reflexive, then there exists a p-morphism of G onto $G_2$ mapping $C_0$ to c and $W -C_0$ to d.

Thus, either $G \twoheadrightarrow G_1$ or $G\twoheadrightarrow G_2$ , and so either ${\textbf {L}}(G)\subseteq {\textbf {L}}(G_1) (= \mathbf {SL4})$ or ${\textbf {L}}(G)\subseteq {\textbf {L}}(G_2) (= \mathbf {S4.1Alt}_2)$ , which proves the lemma.

Proof. In view of Proposition 4.3, it suffices to obtain a Kripke bundle strongly validating $\mathbf {QSL4}$ , but not $B_1$ . We use the Kripke bundle $\mathbb {F}_0$ from the proof of Lemma 4.7. We know that $\mathbb {F}_0 \models ^+ \mathbf {QSL4}$ , so it remains to show that $\mathbb {F}_0 \not \models ^+ B_1$ .

To that end, consider the model $\mathbb {M}_a = (\mathbb {F}_0, \theta )$ where $\theta _u(P) = \{a\}$ . Since, in this model, $u \models P(a)$ , surely $u \models \exists x P(x)$ , and so, by triviality of R, also $u \models \Diamond \square \exists x P(x)$ . On the other hand, since $u \not \models P(b)$ , it follows that $u \not \models \square P(a)$ and $u \not \models \square P(b)$ , and so $u \not \models \exists x \square P(x)$ . Hence, $u \not \models \Diamond \exists x \square P(x)$ .

Proof. The proof is similar to that of the previous lemma. We use the Kripke bundle defined as follows (see Figure 3):

$$ \begin{align*}\begin{array}{cccll} W := \{ u \}, & R := \{ (u, u) \}, & D_u := \{a, b \}, & \rho_{u u} := \{(a, a), (a, b), (b, b) \}, & \\ &&&\kern4pt\mathbb{F}_1 := (W, R, D, \rho). \end{array} \end{align*} $$

Figure 3

Kripke bundle $\mathbb {F}_1$ .

To prove that $\mathbb {F}_1 \models ^+ \mathbf {QS4.1Alt}_2$ , we consider the associated family $\{ F_k = (D_k,R_k) \mid k < \omega \}$ of Kripke frames and show that $F_k \models \mathbf {S4.1Alt}_2$ , for every $k < \omega $ .

Since $F_1$ is isomorphic to the frame $G_2$ from the proof of Lemma 4.10, we know that $F_1 \models \mathbf {S4.1Alt}_2$ .

Now, let $k \geqslant 1$ and let $\mathbf {b} = (b,\ldots ,b) \in D_k$ . We show that, for every $\mathbf {c}\in D_k$ , either both $\mathbf {c}=\mathbf {b}$ and $R_k(\mathbf {c})=\{\mathbf {c}\}$ , or else both $\mathbf {c}\not =\mathbf {b}$ and $R_k(\mathbf {c})=\{\mathbf {c},\mathbf {b}\}$ .

If $\mathbf {c} = \mathbf {b}$ , then, since $\rho (b) = \{ b \}$ , surely $R_k(\mathbf {c}) = R_k(\mathbf {b}) = \{\mathbf {b}\} = \{\mathbf {c}\}$ .

Now, let $\mathbf {c} \ne \mathbf {b}$ and suppose that $\mathbf {e} \in R_k(\mathbf {c})$ . Then, by definition of $\rho $ , for every $i \in \{ 1, \ldots , k\}$ ,

$$ \begin{align*}\begin{array}{lcl} c_i = b & \Longrightarrow & e_i = b\, ( = c_i), \end{array} \end{align*} $$

and either $c_i = a\, \Longrightarrow \, e_i = a\, (= c_i)$ for every i, or $c_i = a\, \Longrightarrow \, e_i = b$ for every i. In the former case, $\mathbf {e} = \mathbf {c}$ , while in the latter, $\mathbf {e} = \mathbf {b}$ . Thus, $R_k(\mathbf {c})=\{\mathbf {c},\mathbf {b}\}$ .

To show that $\mathbb {F}_1 \not \models ^+ B_1$ , we use the model $\mathbb {M}_1 = (\mathbb {F}_1, \theta )$ with $\theta _u(P) = \{a\}$ . In this model, $u \models \exists x P(x)$ , and so $u \models \Diamond \square \exists x P(x)$ . On the other hand, $u \not \models \square P(a)$ and $u \not \models \square P(b)$ , and so $u \not \models \Diamond \exists x\square P(x)$ . Thus, $\mathbb {F}_1 \not \models ^+ B_1$ .

Proof. Assume, for contradiction, that $\boldsymbol {\Lambda } \ne \mathbf {Triv}$ . By Proposition 2.7, $\boldsymbol {\Lambda }$ is Kripke complete. Hence, by Lemma 4.10 and Proposition 2.1(1), either $\mathbf {QK4.1} \subseteq \mathbf {Q}\boldsymbol {\Lambda } \subseteq \mathbf {QSL4}$ or $\mathbf {QK4.1} \subseteq \mathbf {Q}\boldsymbol {\Lambda } \subseteq \mathbf {QS4.1Alt}_2$ . Thus, by Lemma 4.9, $\mathbf {Q}\boldsymbol {\Lambda } \models _{\mathcal {K}} B_1$ , while, by Lemmas 4.12 and 4.13, $\mathbf {Q}\boldsymbol {\Lambda }\not \vdash B_1$ , in contradiction with Kripke completeness of $\mathbf {Q}\boldsymbol {\Lambda }$ .

Proof. Let $\boldsymbol {F} = (W, R, D)$ be a $\mathbf {Q}\boldsymbol {\Lambda }$ -frame. Then, by Proposition 2.4, $(W,R) \models \boldsymbol {\Lambda }$ . By Segerberg–Maksimova theorem [Reference Chagrov and Zakharyaschev1, Theorem 12.21], $\boldsymbol {\Lambda }$ has a finite transitive depth. Hence, every point from W sees a maximal cluster.

To prove that $\boldsymbol {F} \models B_2$ , we consider a model over $\boldsymbol {F}$ and, assuming that, in that model, $u \models \Diamond \square \Diamond \exists x P(x)$ , show that $u \models \Diamond \exists x \square \Diamond P(x)$ .

Since $u \models \Diamond \square \Diamond \exists x P(x)$ , there exists $v\in R(u)$ such that $v \models \square \Diamond \exists x P(x)$ . Let $C\subseteq R(v)$ be a maximal cluster. Then, there exist $w \in C$ and $a \in D_w$ such that $w \models P(a)$ . But then $w \models \square \Diamond P(a)$ : if $t \in C$ , then $D_t = D_w$ and so $a \in D_t$ , which together with $w \in R(t)$ gives us $t \models \Diamond P(a)$ ; since $R(w) = C$ , it then follows that $w \models \square \Diamond P(a)$ . Thus, $w \models \exists x \square \Diamond P(x)$ , and so, by transitivity, $u \models \Diamond \exists x \square \Diamond P(x)$ .

Proof. The argument is similar to that of Lemma 4.10.

It is well known that every locally tabular logic has the finite model property, and so is complete with respect to a class of rooted finite frames. Since $\mathbf {S5} \not \subseteq \boldsymbol {\Lambda }$ , there exists a rooted finite $\boldsymbol {\Lambda }$ -frame $G = (W, R)$ that is not a cluster. Since $\mathbf {D} \subseteq \boldsymbol {\Lambda }$ , the frame G is serial. Let u be the root of G and C the cluster containing u.

We now argue similarly to the proof of Lemma 4.10. If u is irreflexive, there exists a p-morphism from G onto $G_1$ sending u to a and all other points to b. If, on the other hand, u is reflexive, then there exists a p-morphism from G onto $G_2$ mapping C to c and $W-C$ to d. Thus, either $\boldsymbol {\Lambda }\subseteq {\textbf {L}}(G) \subseteq {\textbf {L}}(G_1)(= \mathbf {SL4})$ or $\boldsymbol {\Lambda }\subseteq {\textbf {L}}(G) \subseteq {\textbf {L}}(G_2) (= \mathbf {S4Alt}_2)$ .

Proof. Similar to the proof of Lemma 4.12; we use the Kripke bundle model $\mathbb {M}_a$ defined there. Since we already know that the underlying Kripke bundle validates $\mathbf {QSL4}$ , we only need to show that $\mathbb {M}_a, u \not \models B_2$ .

Since, in this model, $u \models \exists x P(x)$ and R is trivial, it follows that $u \models \Diamond \square \Diamond \exists x P(x)$ . On the other hand, since $u \not \models P(b)$ , it follows that $u \not \models \Diamond P(b)$ ; hence, $u \not \models \square \Diamond P(a)$ and $u \not \models \square \Diamond P(b)$ , and so $u \not \models \exists x \square \Diamond P(x)$ . Thus, $u \not \models \Diamond \exists x \square \Diamond P(x)$ , due to triviality of R.

Proof. Similar to the proof of Lemma 4.13; we use the Kripke bundle $\mathbb {F}_1$ and the model $\mathbb {M}_1$ defined there. We only need to show that $\mathbb {M}_1, u \not \models B_2$ .

In this model, $u \models \exists xP(x)$ , and so $u \models \Diamond \square \Diamond \exists x P(x)$ . On the other hand, $u \not \models \Diamond P(b)$ , and so $u \not \models \square \Diamond P(a)$ and $u \not \models \square \Diamond P(b)$ . Hence, $u \not \models \exists x\square \Diamond P(x)$ , and so $u \not \models \Diamond \exists x\square \Diamond P(x)$ .

Proof. Similar to the proof of Theorem 4.14. By Lemmas 4.15, 4.18, and 4.19, $\boldsymbol {\Lambda }\not \subseteq \textbf {SL4}$ and $\boldsymbol {\Lambda }\not \subseteq \textbf {S4Alt}_2$ . Hence, by Lemma 4.16, $\mathbf {S5} \subseteq \boldsymbol {\Lambda }$ .

Proof. It is not hard to see that the propositional logic $\mathbf {SL4}$ has only two Kripke frames: a reflexive singleton and a frame isomorphic to the frame $G_1$ from the proof of Lemma 4.10. So, in every QSL4-frame, starting from any world, in a single step we reach a reflexive world; this world validates $\forall \mathit {ref}$ .

Proof. In view of Lemma 5.1, it suffices to show that $L_0$ is Kripke complete. Due to Theorem 3.21, it is enough to prove that $L_0$ is quasi-canonical. Let $C(\Gamma )$ be defined as in $\S $ 3.

First, we notice that, if $\Gamma \in W_{L_0}$ , then $C(\Gamma )$ is a singleton: since $L_0 \vdash \Diamond \top $ , we know that $\Diamond \top \in \Gamma $ and so, by Existence lemma, $C(\Gamma ) \ne \varnothing $ ; also, $L_0 \vdash \boldsymbol {alt}_1$ , and so, by Lemma 3.24, $|C(\Gamma )| \leqslant 1$ .

Now, suppose that $\Gamma \in W_{L_0}$ . To prove the existence of a quasi-canonical model containing $\Gamma $ , we consider two cases.

Case $C(\Gamma ) = \{\Gamma \}$ : In this case, $\boldsymbol {M}_{L_0}\upharpoonright \{\Gamma \}$ is a weak selective submodel of $\boldsymbol {M}_{L_0}$ since $\Diamond A \to \square A \in \Gamma $ , for every $A \in \mathcal {L}(\Gamma )$ , and $\square ^- \Gamma \subseteq \Gamma $ . Also, the base predicate frame $\boldsymbol {F}$ validates $L_0$ : since the underlying Kripke frame F is a reflexive singleton, surely $F \models \mathbf {SL4}$ , and so, by Proposition 2.4, $\boldsymbol {F} \models \mathbf {QSL4}$ ; moreover, by Lemma 5.1, $\mathbf {QSL4} \models _{\mathcal {K}} \square \forall \mathit {ref}$ , and so $\boldsymbol {F} \models \square \forall \mathit {ref}$ .

Case $C(\Gamma ) = \{{\Delta }\}$ , with ${\Delta } \ne \Gamma $ : We start by showing that, in this case, ${\Delta } R_{L_0} {\Delta }$ .

First, we note that $\mathbf {SL4} \vdash \square \boldsymbol {ref}$ , which can be shown either semantically, using Kripke completeness of $\mathbf {SL4}$ , or syntactically, using

$$ \begin{align*}\begin{array}{ll} &\mathbf{SL4}\vdash\square(\square P \rightarrow P)\,{\leftrightarrow}\,(\square\square P \rightarrow \square P) \quad \text{and} \quad \\ &\mathbf{SL4}\vdash (\square\square P \rightarrow \square P)\,{\leftrightarrow}\, (\Diamond\Diamond P \rightarrow \Diamond P). \end{array} \end{align*} $$

Second, by [Reference Shehtman7, Proposition 3.10], $L_0 \vdash \square A$ whenever $A\in \mathbf {QT}$ ; in particular, $L_0 \vdash \square \overline {\forall } (\square B\rightarrow B)$ , for every formula B. Thus, by Lemma 3.2(1), $\square \overline {\forall } (\square B\rightarrow B)\in \Gamma $ , and so, since $\Gamma R_{L_0} {\Delta }$ ,

(5.1) $$ \begin{align} \overline{\forall} (\square B\rightarrow B)\in{\Delta}. \end{align} $$

Now, to prove that ${\Delta } R_{L_0} {\Delta }$ , we assume that $\square C(\mathbf {a})\in {\Delta }$ , where $\mathbf {a}$ is a list of constants, to show that $C(\mathbf {a})\in {\Delta }$ . Since, by (5.1),

$$ \begin{align*}\forall\mathbf{x} (\square C(\mathbf{x})\rightarrow C(\mathbf{x}))\in{\Delta}, \end{align*} $$

it follows that

$$ \begin{align*}\square C(\mathbf{a})\rightarrow C(\mathbf{a})\in{\Delta}, \end{align*} $$

and so, by (MP), $C(\mathbf {a})\in {\Delta }$ .

Since ${\Delta } R_{L_0} {\Delta }$ , we know that ${\Delta } \in C(\Delta )$ , and so, since $C(\Delta )$ is a singleton, ${C(\Delta ) = \{{\Delta }\}}$ . It follows that $\boldsymbol {M}_{L_0}\upharpoonright \{\Gamma ,{\Delta }\}$ is a selective weak submodel of $\boldsymbol {M}_{L_0}$ . The underlying Kripke frame $\boldsymbol {F} := \boldsymbol {F}_{L_0}\upharpoonright \{\Gamma ,{\Delta }\}$ is isomorphic to the frame $G_1$ from the proof of Lemma 4.10, and so $\boldsymbol {F} \models \mathbf {SL4}$ . Then, by Proposition 2.4, Lemma 5.1, and Soundness theorem, $\boldsymbol {F} \models L_0$ .

Proof. Let $L_1:=\mathbf { QK4Alt}_1 + A_1$ . In view of (5.2), it suffices to prove that $L_1$ is Kripke complete. Again, we show that $L_1$ is quasi-canonical. To this end, we prove a series of lemmas.

Proof. Since $\mathbf {K} + \Diamond ^2\top \vdash \Diamond \top $ , it follows that $L_1+\Diamond ^2\top \supseteq \mathbf { QSL4}$ . Also, due to $A_1$ ,

$$ \begin{align*}L_1+\Diamond^2\top\vdash \Diamond\forall ref, \end{align*} $$

and so, due to $\boldsymbol {alt}_1$ ,

$$ \begin{align*}L_1 + \Diamond^2\top\vdash\square\forall ref. \end{align*} $$

Hence, $L_0 \subseteq L_1+\Diamond ^2\top $ .

The converse inclusion $L_1 + \Diamond ^2\top \subseteq L_0$ holds since $\mathbf {K4Alt}_1\subseteq \mathbf {SL4}$ , $\mathbf {SL4} \vdash \Diamond ^2\top $ , and $\mathbf {QSL4}\vdash \square \forall \mathit {ref} \rightarrow \Diamond \forall \mathit {ref}$ .

Proof. Let

$$ \begin{align*}\begin{array}{lcl} \boldsymbol{\Lambda}_0 & := & \mathbf{Alt}_1+\Diamond^2\top\rightarrow\square(\square P \rightarrow P). \end{array} \end{align*} $$

Then, by substitution,

$$ \begin{align*}\boldsymbol{\Lambda}_0 \vdash\Diamond^2\top\rightarrow\square(\square^2\bot\rightarrow \square\bot), \end{align*} $$

and so, by $\mathbf {K}$ ,

$$ \begin{align*}\boldsymbol{\Lambda}_0 \vdash\Diamond^2\top\rightarrow(\Diamond\square^2\bot\rightarrow \Diamond\square\bot). \end{align*} $$

Hence, by $\boldsymbol {alt}_1$ ,

$$ \begin{align*}\boldsymbol{\Lambda}_0 \vdash\Diamond^2\top\rightarrow(\Diamond\square^2\bot\rightarrow \square^2\bot), \end{align*} $$

and so, by classical logic,

(5.3) $$ \begin{align} \boldsymbol{\Lambda}_0 \vdash\Diamond^2\top\rightarrow\square\Diamond^2\top. \end{align} $$

Hence, by monotonicity of $\square $ , for every $k \geqslant 0$ ,

(5.4) $$ \begin{align} \boldsymbol{\Lambda}_0 \vdash\square^k \Diamond^2\top\rightarrow\square^{k+1}\Diamond^2\top. \end{align} $$

Eventually, by induction on n, using (5.3) and (5.4), we obtain that, for every $n \geqslant 0$ ,

$$ \begin{align*}\boldsymbol{\Lambda}_0 \vdash\Diamond^2\top\rightarrow\square^n\Diamond^2\top.\end{align*} $$

Proof. We use deduction theorems from [Reference Gabbay, Shehtman and Skvortsov2]. By Lemma 5.4, $L_0=L_1+\Diamond ^2\top $ . So assume that $L_1+\Diamond ^2\top \vdash B$ . Then, by [Reference Gabbay, Shehtman and Skvortsov2, Theorem 2.8.4],

$$ \begin{align*}\square^\infty\Diamond^2\top\vdash_{L_1} B. \end{align*} $$

Thus, for some $n \geqslant 0$ ,

(5.5) $$ \begin{align} \Diamond^2\top,\square\Diamond^2\top,\ldots,\square^n\Diamond^2\top\vdash_{L_1} B. \end{align} $$

Due to $\boldsymbol {alt}_1$ and the substitution into $A_1$ ,

$$ \begin{align*}L_1 \vdash \Diamond^2\top\rightarrow\square(\square P \rightarrow P). \end{align*} $$

Hence, by Lemma 5.5, for every $n \geqslant 0$ ,

$$ \begin{align*}L_1\vdash\Diamond^2\top\rightarrow\square^n\Diamond^2\top, \end{align*} $$

and so, by (5.5),

$$ \begin{align*}\Diamond^2\top\vdash_{L_1} B. \end{align*} $$

Hence, by Deduction theorem,

$$ \begin{align*}L_1 \vdash \Diamond^2\top\rightarrow B. \end{align*} $$

Proof. Since $\mathbf {K} \vdash \square ^2 \bot \to \square ^2 P$ , and so $\mathbf {K} \vdash \square ^2 \bot \to (\square P \to \square ^2 P)$ , it follows that

$$ \begin{align*}\mathbf{K4}\subseteq\mathbf{K}+\square^2 \bot. \end{align*} $$

Also, by classical logic,

$$ \begin{align*}\mathbf{QK}+\square^2\bot\vdash A_1. \end{align*} $$

Hence, $L_1+\square ^2\bot \subseteq L_2$ . The converse inclusion is trivial.

Proof. By Lemma 5.7, $L_2 = L_1 + \square ^2\bot $ . So assume that $ L_1 + \square ^2\bot \vdash B$ . It follows, as in the proof of Lemma 5.6, that, for some $n \geqslant 2$ ,

$$ \begin{align*}\square^2\bot,\ldots,\square^n\bot\vdash_{L_1} B. \end{align*} $$

Since, for every $m \geqslant 2$ ,

$$ \begin{align*}\mathbf{K}\vdash\square^2\bot\rightarrow\square^m\bot, \end{align*} $$

it follows that $\square ^2\bot \vdash _{L_1} B$ , and hence, $L_1\vdash \square ^2\bot \rightarrow B$ .

Proof. The inclusion $L_1\subseteq L_0\cap L_2$ follows immediately from Lemmas 5.4 and 5.7.

For the converse, assume that $A\in L_0\cap L_2$ . Then, by Lemma 5.6, $L_1\vdash \Diamond ^2\top \rightarrow A$ and, by Lemma 5.8, $L_1\vdash \square ^2\bot \rightarrow A$ . Since $\mathbf {K}\vdash \Diamond ^2\top \vee \square ^2\bot $ , it follows that $L_1\vdash A$ .

We now complete the proof of Theorem 5.3: By Theorems 3.23 and 3.26, $L_2$ is quasi-canonical. As we have seen in the proof of Theorem 5.2, $L_0$ is also quasi-canonical. Hence, by Lemma 5.9 and Proposition 3.28, $L_1$ is quasi-canonical.

Proof. Let $\boldsymbol {F} = (W,R,D)$ be a $\mathbf {QS4Alt}_2$ -frame and let $\boldsymbol {M}$ be a model over $\boldsymbol {F}$ . Supposing that $\boldsymbol {M},u \not \models q$ , we show that $\boldsymbol {M},u \models \square (q\rightarrow \overline {\forall }C^{+n})$ , for every $n \geqslant 1$ .

Assume that $uRv$ and $\boldsymbol {M},v \models q$ . Then, $u \ne v$ . Since $(W,R) \models \mathbf {S4Alt}_2$ , it follows that $R(u)=\{u,v\}$ and $R(v)=\{v\}$ . Hence, for all $a_1,\ldots ,a_n\in D_v$ ,

$$ \begin{align*}\boldsymbol{M}, v \models \Diamond P^n(a_1,\ldots,a_n)\rightarrow P^n(a_1,\ldots,a_n), \end{align*} $$

and so $\boldsymbol {M}, v \models \overline {\forall }C^{+n}$ . Since $R(u)=\{u,v\}$ and $\boldsymbol {M},u \not \models q$ , it follows that $\boldsymbol {M}, u \models \square (q\rightarrow \overline {\forall }C^{+n})$ .

Proof. In view of Lemma 5.10, it suffices to prove that $L_3$ is Kripke complete; to that end, we show that $L_3$ is quasi-canonical.

Let $\Gamma $ be an $L_3$ -place. Since $L_3 \vdash \square P \to P$ , the canonical frame $\boldsymbol {F}_{L_3}$ is reflexive. Arguing as in the proof of Lemma 3.24, we see that $|C(\Gamma )| \leqslant 2$ ; moreover, due to reflexivity, we may assume that $\Gamma \in C^\circ (\Gamma )$ . We consider two cases.

Case $C^\circ (\Gamma ) =\{\Gamma \}$ : In this case, $\boldsymbol {M}_{L_3}\upharpoonright \{ \Gamma \} $ is a selective submodel of $\boldsymbol {M}_{L_3}$ . The underlying predicate Kripke frame $\boldsymbol {F}$ is a reflexive singleton with a domain; hence, $\boldsymbol {F} \models \mathbf {QTriv}$ , and so, since $\mathbf {QS4Alt}_2 \subseteq \mathbf {QTriv}$ , also $\boldsymbol {F} \models \mathbf {QS4Alt}_2$ . Thus, by Lemma 5.10, $\boldsymbol {F} \models L_3$ .

Case $C^\circ (\Gamma ) = \{\Gamma ,{\Delta }\}$ , with ${\Delta }\neq \Gamma $ : In this case, there exists a $D_\Gamma $ -sentence A such that $A \notin \Gamma $ and $A \in \Delta $ . Then, by Lemma 3.3, $\Diamond A\in \Gamma $ . By substitution, for every formula B,

$$ \begin{align*}L_3\vdash A\vee\square(A\rightarrow\overline{\forall}(\Diamond B\rightarrow B)), \end{align*} $$

and so, since $A\not \in \Gamma $ , we know that $\square (A\rightarrow \overline {\forall }(\Diamond B\rightarrow B))\in \Gamma $ . Then, since $\square ^-\Gamma \subseteq {\Delta }$ , it follows that $A\rightarrow \overline {\forall }(\Diamond B\rightarrow B)\in {\Delta }$ .

Now, let $\Theta $ be an $L_{3}$ -place containing ${\Delta }$ . Then, $A, A\rightarrow \overline {\forall }(\Diamond B\rightarrow B)\in \Theta $ , and so, by (MP), for every formula B,

(5.6) $$ \begin{align} \overline{\forall}(\Diamond B\rightarrow B)\in\Theta. \end{align} $$

But then $\boldsymbol {M} := \boldsymbol {M}_{L_3}\upharpoonright \{\Gamma ,\Theta \}$ is selective: if $\Diamond B(\mathbf {a})\in \Theta $ , for a $D_\Theta $ -sentence $B(\mathbf {a})$ , then, due to (5.6), $\Diamond B(\mathbf {a})\rightarrow B(\mathbf {a}) \in \Theta $ , and so $B(\mathbf {a}) \in \Theta $ . That $\boldsymbol {M}$ is based on an $L_3$ -frame is proved as in the preceding case.