2 Preliminaries

In this section, we briefly recall products of modal logics and their relationship to mm-logics.

Definition 2.1 [Reference Gabbay and Shehtman13, Definition 3.6].

Let $\mathfrak {F}=(X_1,R_1)$ and $\mathfrak {G}=(X_2,R_2)$ be Kripke frames. The product of $\mathfrak {F}$ and $\mathfrak {G}$ is the frame

$$ \begin{align*}\mathfrak{F}\times\mathfrak{G}=(X_1\times X_2, R_1^\vee, R_2^\vee)\end{align*} $$

where the relations $R_1^\vee , R_2^\vee $ are defined on $X_1\times X_2$ as follows for any $(x_1,x_2),(y_1,y_2)\in X_1\times X_2$ :

$$ \begin{align*} (x_1,x_2)\mathrel{R_1^\vee}(y_1,y_2) &\iff x_1\mathrel{R_1}y_1\text{ and }x_2=y_2,\\ (x_1,x_2)\mathrel{R_2^\vee}(y_1,y_2) &\iff x_1=y_1\text{ and }x_2\mathrel{R_2}y_2. \end{align*} $$

As we pointed out in the introduction, we will only work with product frames $\mathfrak {F}\times \mathfrak {G}$ where $\mathfrak {G}$ is an $\mathbf{S5}$ -frame (i.e., $R_2$ is an equivalence relation). It is then straightforward to check that $R_2^\vee $ is an equivalence relation. We thus simplify our notation and denote $R_1^\vee $ by R and $R_2^\vee $ by E. Let $\mathfrak {F}\times \mathfrak {G}=(X_1\times X_2,R,E)$ be a product frame. It is well known (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, p. 222]) that the following first-order properties hold in $\mathfrak {F}\times \mathfrak {G}$ :

1. (LC) Left commutativity:

   ${(\forall a,b,c{\kern-1.5pt}\in{\kern-1.5pt} X_1{\kern-1.5pt}\times{\kern-1.5pt} X_2)(a{\kern-1.5pt}\mathrel {E}{\kern-1.5pt}b \text { and } b{\kern-1.5pt}\mathrel {R}{\kern-1.5pt} c) {\kern-2pt}\implies{\kern-2pt} (\exists d {\kern-1.5pt}\in{\kern-1.5pt} X_1 {\kern-1.5pt}\times{\kern-1.5pt} X_2)(a{\kern-1.5pt}\mathrel {R}{\kern-1.5pt} d \text { and } d{\kern-1.5pt}\mathrel {E}{\kern-1.5pt} c)}$ .

   

1. (RC) Right commutativity:

   ${(\forall a,b,c{\kern-1.5pt}\in{\kern-1.5pt} X_1{\kern-1.5pt}\times{\kern-1.5pt} X_2)(a{\kern-1.5pt}\mathrel {R}{\kern-1.5pt}b \text { and } b{\kern-1.5pt}\mathrel {E}{\kern-1.5pt} c) {\kern-1.5pt}\implies{\kern-1.5pt} (\exists d {\kern-1.5pt}\in{\kern-1.5pt} X_1 {\kern-1.5pt}\times{\kern-1.5pt} X_2)(a{\kern-1.5pt}\mathrel {E}{\kern-1.5pt} d \text { and } d{\kern-1.5pt}\mathrel {R}{\kern-1.5pt} c)}$ .

   

These first-order properties can be expressed modally. To do so, we first supply the necessary syntactic details. We follow the convention that a modal logic $\mathbf{L}$ is formulated in the propositional language $\mathcal {L}_\Diamond $ with the modality $\Diamond $ , while $\mathbf{S5}$ is expressed in the propositional language $\mathcal {L}_\exists $ with the modality $\exists $ . As usual, $\Box $ and $\forall $ abbreviate $\neg \Diamond \neg $ and $\neg \exists \neg $ , respectively. Let $\mathcal {L}_{\Diamond \exists }$ denote the propositional language with two modalities $\Diamond $ and $\exists $ .

Let

$$ \begin{align*}\text{com}^l = \exists\Diamond p\to \Diamond\exists p \quad \text{and} \quad \text{com}^r = \Diamond\exists p \to \exists\Diamond p.\end{align*} $$

Motivated by the connection to predicate modal logic (see Section 6 for details), we refer to $\text {com}^r$ as the monadic Barcan formula and to $\text {com}^l$ as the converse monadic Barcan formula.

Definition 2.3. For a propositional modal logic $\mathbf{L}$ , let

$$ \begin{align*}\mathbf{ML} = (\mathbf{L}\otimes \mathbf{S5}) + \text{com}^l \quad \text{and} \quad \mathbf{MLB} = (\mathbf{L}\otimes \mathbf{S5}) + \text{com}^l + \text{com}^r.\end{align*} $$

We note that in the literature on product logics, $\mathbf {ML}$ is typically denoted by $[\mathbf {L},\mathbf {S5}]^{\text {EX}}$ and $\mathbf {MLB}$ by $[\mathbf {L},\mathbf {S5}]$ (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12]). Our terminology is motivated by the connection to predicate modal logic (see Section 6 for details). For the same reason, we call $\mathbf {ML}$ the monadic extension of $\mathbf {L}$ . In particular, $\mathbf {MK}$ is the monadic extension of the least propositional normal modal logic $\mathbf {K}$ .

The fusion $\mathbf {L}\otimes \mathbf {S5}$ is interpreted in a $2$ -frame $\mathfrak {F}=(X,R,E)$ , where R is a binary relation and E is an equivalence relation on X (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, p. 21]). In the $2$ -frame $\mathfrak {F}$ , the relation R interprets the modality $\Diamond $ , while the equivalence relation E is reserved for the modality $\exists $ . Therefore, an $(\mathbf {L}\otimes \mathbf {S5})$ -frame is a $2$ -frame $\mathfrak {F}=(X,R,E)$ such that the reduct $(X,R)$ is an $\mathbf {L}$ -frame (meaning that $(X,R) \models \mathbf {L}$ ) and $(X,E)$ is an $\mathbf {S5}$ -frame (meaning that $(X,E)\models \mathbf {S5}$ ).

It is straightforward to verify (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, p. 222]) that left and right commutativity are definable in $\mathcal {L}_{\Diamond \exists }$ by $\text {com}^l$ and $\text {com}^r$ . Consequently, an $(\mathbf {L}\otimes \mathbf {S5})$ -frame $\mathfrak {F}=(X,R,E)$ is an $\mathbf {MK}$ -frame iff it satisfies (LC), and an $\mathbf {MKB}$ -frame iff it additionally satisfies $\text {com}^r$ .

Since product frames $\mathfrak {F}\times \mathfrak {G}$ are $\mathbf {MKB}$ -frames, both $\text {com}^l$ and $\text {com}^r$ are provable in $\mathbf {L}\times \mathbf {S5}$ . Therefore, $\mathbf {MLB}\subseteq \mathbf {L}\times \mathbf {S5}$ (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, Proposition 3.8]). However, the other inclusion may not hold.

Since we are interested in the logics $\mathbf {Grz}\times \mathbf {S5}$ and $\mathbf {GL}\times \mathbf {S5}$ , we recall the semantics for $\mathbf {Grz}$ and $\mathbf {GL}$ . It is well known that

• • $\mathbf {Grz}$ is the logic of Noetherian posets, that is, posets without infinite ascending chains (see, e.g., [Reference Chagrov and Zakharyaschev7, Corollary 5.52(i)]);

• • $\mathbf {GL}$ is the logic of Noetherian strict orders, that is, strict orders without infinite ascending chains (see, e.g., [Reference Chagrov and Zakharyaschev7, Corollary 5.47(i)]).

We will also work with $\mathbf {Grz}$ and $\mathbf {GL}$ in the presence of the finite depth formulae, which are given by

$$ \begin{align*} bd_1&=\Diamond\Box p_1\to p_1,\\ bd_n&=\Diamond(\Box p_n\wedge \neg bd_{n-1})\to p_n. \end{align*} $$

These formulae express the finiteness of the depth of a transitive frame. To this end, we recall the following definition.

The following result is a direct adaptation of a well-known result to the monadic setting.

For any logic $\mathbf{L}$ , we denote by $\mathbf {L}[n]$ the extension of $\mathbf{L}$ with the finite depth formula $bd_n$ . By Proposition 2.8, $\mathbf {Grz}[n]$ -frames are precisely the $\mathbf {Grz}$ -frames of depth at most n. Similarly, $\mathbf {GL}[n]$ -frames can be identified as $\mathbf {GL}$ -frames having depth at most n. In the next section we will show that $\mathbf {GL}[n]\times \mathbf {S5}$ and $\mathbf {Grz}[n]\times \mathbf {S5}$ are finitely axiomatizable for each $n\geq 1$ .

3 Axiomatizing $\mathbf {Grz}[n]\times \mathbf {S5}$

As we pointed out in the introduction, product matching is not a common phenomenon. For our purposes, we recall that neither $\mathbf {Grz}\times \mathbf {S5}$ nor $\mathbf {Grz}[n]\times \mathbf {S5}$ ( $n\geq 2$ ) is product matching (see [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, Theorem 5.17]). We will show that these product logics are finitely axiomatizable. In fact, we will prove that they can be axiomatized by adding the Gödel translation of the monadic Casari formula

$$ \begin{align*}\forall((p\to\forall p)\to\forall p)\to\forall p,\end{align*} $$

which plays an important role in lifting the well-known translations

$$\begin{align*}\mathbf{IPC} \hookrightarrow \mathbf{Grz} \hookrightarrow \mathbf{GL} \end{align*}$$

to the monadic setting [Reference Bezhanishvili, Brantley and Ilin4]. In this section, we concentrate on $\mathbf {Grz}[n]\times \mathbf {S5}$ , and deal with $\mathbf {Grz}\times \mathbf {S5}$ in Section 5.

Recall from Definition 2.3 that $\mathbf {MGrz}$ is the monadic extension of $\mathbf {Grz}$ , and that adding the monadic Barcan formula to $\mathbf {MGrz}$ results in the mm-logic $\mathbf {MGrzB}$ . We adopt the following from [Reference Bezhanishvili, Brantley and Ilin4, Definition 4.5]:

Definition 3.1. Let

$$ \begin{align*} \mathbf{M}^+\mathbf{Grz}&=\mathbf{MGrz}+\Box\forall(\Box(\Box p\to \Box\forall p)\to\Box\forall p)\to\Box\forall p,\\ \mathbf{M}^+\mathbf{GrzB}&=\mathbf{MGrzB}+\Box\forall(\Box(\Box p\to \Box\forall p)\to\Box\forall p)\to\Box\forall p. \end{align*} $$

To give a semantic characterization of the Casari formula, we recall that for a binary relation S on a set X, the S-image of $x \in X$ is the set $S[x]:=\{y\in X\mid x\mathrel {S}y\}$ . If S is an equivalence relation, then we refer to $S[x]$ as an S-cluster.

Example 3.4. A typical example of an $\mathbf{MGrz}$ -frame with a dirty cluster is the following frame:

Here, $X=\{x,y\}$ , $R=\{(x,x),(x,y),(y,y)\}$ , and $E=X^2$ (where the circles represent reflexive points, the black arrow indicates the non-reflexive relation $(x,y)$ , and the blue curve depicts the equivalence relation E). Observe that this is in fact an $\mathbf {MGrzB}$ -frame which refutes the Casari formula. Indeed, let $v$ be a valuation for which $v(p)=\{y\}$ . Then $y \models \Box p$ , but $y \not \models \Box \forall p$ , so $y\not \models \Box (\Box p \to \Box \forall p)$ . Since $x \mathrel {R} y$ , we also have $x\not \models \Box (\Box p \to \Box \forall p)$ . Thus, $x\models \Box \forall (\Box (\Box p\to \Box \forall p)\to \Box \forall p)$ . On the other hand, $x\not \models \Box \forall p$ , showing that the Casari formula is refuted on this frame.

The next result was proved in [Reference Bezhanishvili, Brantley and Ilin4, Lemma 4.8] for descriptive $\mathbf {MGrz}$ -frames, but since $\mathbf {MGrz}$ -frames have no infinite ascending R-chains (so all nonempty subsets of $\mathbf {MGrz}$ -frames have maximal points), the same proof yields the following.

To prove that $\mathbf {Grz}[n]\times \mathbf {S5} = \mathbf {M}^+\mathbf {GrzB}[n]$ , we show that the embedding $\mathbf {Grz}[n] \hookrightarrow \mathbf {GL}[n]$ extends to yield the embeddings $\mathbf {M}^+\mathbf {Grz}[n] \hookrightarrow \mathbf {MGL}[n]$ and $\mathbf {M}^+\mathbf {GrzB}[n] \hookrightarrow \mathbf {MGLB}[n]$ . To recall the former, for each formula $\varphi $ , let $\varphi ^+$ denote the formula obtained by replacing every instance of $\Box \psi $ in $\varphi $ with $\Box ^+\psi := \psi \wedge \Box \psi $ . It is well known (see, e.g., [Reference Chagrov and Zakharyaschev7, Theorem 3.88]) that

$$ \begin{align*}\mathbf{Grz}\vdash\varphi \iff \mathbf{GL}\vdash\varphi^+,\end{align*} $$

thus yielding an embedding of $\mathbf {Grz}$ into $\mathbf {GL}$ , which further gives an embedding of $\mathbf {Grz}[n]$ into $\mathbf {GL}[n]$ for each $n\ge 1$ .

Definition 3.7 [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, p. 228].

A Kripke complete logic $\mathbf {L}$ is Horn axiomatizable if the class of $\mathbf {L}$ -frames can be axiomatized by closed formulae or by the formulae that correspond to first-order sentences of the form

$$ \begin{align*} \forall x\forall y\forall \vec{z} \big(\psi(x,y,\vec{z})\to R(x,y)\big), \end{align*} $$

where $\psi (x,y,\vec{z})$ is a positive formula.

The following result justifies the importance of Horn axiomatizable unimodal logics.

Since $\mathbf {Grz}[n]\times \mathbf {S5}$ is not product matching for $n \ge 2$ , we conclude from Theorem 3.8 that $\mathbf {Grz}[n]$ is not Horn axiomatizable. On the other hand, each $\mathbf {GL}[n]$ is Horn axiomatizable. To see this, note that $\mathbf {GL}[n]=\mathbf {K4}+\neg \Diamond ^n \top $ for each $n \ge 1$ . Indeed, for a Kripke frame $\mathfrak F=(X,R)$ , we have $\mathfrak F\models \neg \Diamond ^n\top $ iff $R^n=\varnothing $ . In particular, $\mathfrak F\models \neg \Diamond ^n\top $ implies that every point in $\mathfrak F$ is irreflexive. When $\mathfrak F$ is transitive, the condition $R^n=\varnothing $ also implies that $d(\mathfrak {F})\leq n$ , yielding that $\mathfrak F \models \mathbf {K4}+\neg \Diamond ^n\top $ iff $\mathfrak F$ is a transitive irreflexive frame of depth $\le n$ . Therefore, $\mathbf{K4} + \neg \Diamond^n \top$ is the logic of such frames (see, e.g., [Reference Chagrov and Zakharyaschev7, Theorem 6.15]). Since $\mathbf {GL}[n]$ is also the logic of such frames (see, e.g., [Reference Kracht19, p. 429]), $\mathbf {GL}[n]=\mathbf {K4}+\neg \Diamond ^n \top $ . Thus, $\mathbf {GL}[n]$ is Horn axiomatizable because so is $\mathbf {K4}+\neg \Diamond ^n\top $ . This together with Theorem 3.8 yields the following corollary.

To lift the translation $\mathbf {Grz}[n] \hookrightarrow \mathbf {GL}[n]$ to the monadic setting, we extend the reflexivization and irreflexivization operations from Kripke frames to $\mathbf {MK}$ -frames.

Let $\mathfrak {F}=(X,R)$ be a Kripke frame. We recall (see, e.g., [Reference Chagrov and Zakharyaschev7, p. 98]) that the reflexivization of $\mathfrak F$ is the Kripke frame $\mathfrak {F}^r=(X,R^r)$ , where $R^r$ is the reflexive closure of R; that is,

$$\begin{align*}x\mathrel{R^r}y\iff x\mathrel{R}y \text{ or } x=y. \end{align*}$$

We also recall that the irreflexivization of $\mathfrak F$ is the Kripke frame $\mathfrak {F}^{ir}=(X,R^{ir})$ , where $R^{ir}$ is the irreflexive fragment of R; that is,

$$\begin{align*}x\mathrel{R^{ir}}y\iff x\mathrel{R}y \text{ and } x\neq y. \end{align*}$$

These notions naturally extend to $\mathbf {MK}$ -frames.

The same proof as in [Reference Chagrov and Zakharyaschev7, Lemma 3.86] yields the following lemma.

Lemma 3.14. Let $\mathfrak {F}=(X,R,E)$ be an $\mathbf {MK}$ -frame. Then for any $\mathcal {L}_{\Diamond \exists }$ -formula $\varphi $ ,

$$ \begin{align*} \mathfrak{F}\models\varphi^+\iff\mathfrak{F}^r\models\varphi. \end{align*} $$

For the next result, which is a generalization of [Reference Bezhanishvili, Brantley and Ilin4, Lemma 4.10], we point out that every $\mathbf {MGL}$ -frame has only clean E-clusters. To see this, let $\mathfrak {F}=(X,R,E)$ be an $\mathbf {MGL}$ -frame and let $u,v\in E[x]$ . If $u\mathrel {R}v$ , then by left commutativity, ${R[x]\cap E[x]\neq \varnothing }$ . Let $x_1\in R[x]\cap E[x]$ . Then $x\neq x_1$ since R is irreflexive. Continuing this process produces an infinite chain $x\mathrel {R}x_1\mathrel {R}x_2\dots $ in $E[x]$ , which is impossible (since R is a Noetherian strict order).

By [Reference Bezhanishvili, Brantley and Ilin4, Theorem 4.12], $\varphi \in \mathbf {M}^+\mathbf {Grz}\iff \varphi ^+\in \mathbf {MGL}$ . To obtain a similar result for the logics in the previous lemma, we require the following.

Theorem 3.19. For an $\mathcal {L}_{\Diamond \exists }$ -formula $\varphi $ ,

$$ \begin{align*}\varphi\in\mathbf{M}^+\mathbf{GrzB}[n]\iff \varphi^+\in\mathbf{MGLB}[n].\end{align*} $$

Remark 3.20. Following the same line of reasoning (see Remark 3.16), we have

$$ \begin{align*}\varphi\in\mathbf{M}^+\mathbf{Grz} [n]\iff \varphi^+\in\mathbf{MGL}[n].\end{align*} $$

We are ready to prove the main result of this section.

Proof. As we already pointed out in Remark 3.6, $\mathbf {M}^+\mathbf {GrzB}[n]\subseteq \mathbf {Grz}[n]\times \mathbf {S5}$ . For the reverse inclusion, let $\varphi \notin \mathbf {M}^+\mathbf {GrzB}[n]$ . By Theorem 3.19, $\varphi ^+\notin \mathbf {MGLB}[n]$ . By Corollary 3.10, there is a $(\mathbf {GL}[n]\times \mathbf {S5})$ -frame $\mathfrak {F}\times \mathfrak {G}$ such that $\mathfrak {F}\times \mathfrak {G}\not \models \varphi ^+$ . Therefore, $(\mathfrak {F}\times \mathfrak {G})^r\not \models \varphi $ by Lemma 3.14. But $(\mathfrak {F}\times \mathfrak {G})^r=\mathfrak {F}^r\times \mathfrak {G}$ since for any $(\mathbf {K}\times \mathbf {S5})$ -frame $\mathfrak {X}\times \mathfrak {Y}$ we have $(\mathfrak {X}\times \mathfrak {Y})^r=\mathfrak {X}^r\times \mathfrak {Y}.$ To see this, let $\mathfrak {X}=(X,R_X)$ and $\mathfrak {Y}=(Y,E_Y)$ . Then $\mathfrak {X}\times \mathfrak {Y}=(X\times Y, R, E)$ and $\mathfrak {X}^r\times \mathfrak {Y}=(X\times Y, R',E)$ , where R, $R'$ , and E are defined as in Definition 2.1. It suffices to show that $R' = R^r$ . Let $(x,y), (u,v)\in X\times Y$ . Then,

$$ \begin{align*} (x,y)\mathrel{R'}(u,v) &\iff (x\mathrel{R_X^r} u \text{ and } y=v)\\ &\iff ((x\mathrel{R_X}u \text{ or } x=u) \text{ and } y=v)\\ &\iff (x,y)\mathrel{R}(u,v) \text{ or } (x,y)=(u,v)\\ &\iff (x,y)\mathrel{R^r}(u,v). \end{align*} $$

Since $\mathfrak {F}$ is a $\mathbf {GL}[n]$ -frame, $\mathfrak {F}^r$ is a $\mathbf {Grz}[n]$ -frame (see the proof of Lemma 3.15(1)). Hence, $\varphi $ is refuted in a $(\mathbf {Grz}[n]\times \mathbf {S5})$ -frame. Thus, $\varphi \notin \mathbf {Grz}[n]\times \mathbf {S5}$ , and so $\mathbf {Grz}[n]\times \mathbf {S5}=\mathbf {M}^+\mathbf {GrzB}[n]$ .

4 Selective filtration for $\mathbf{MGrzB}$

In this section, we show that $\mathbf {MGrzB}$ admits a form of selective filtration. This will be utilized in Section 5 to show that $\mathbf{MGrzB}$ has the fmp. With appropriate adjustments, we also establish the fmp for $\mathbf {M}^+\mathbf {GrzB}$ and $\mathbf {MGLB}$ . The selective filtration method employed here is a refinement of the construction developed in [Reference Bezhanishvili and Khan6], which itself synthesizes the approaches of [Reference Bezhanishvili, Brantley and Ilin4, Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, Reference Grefe16]. The need of the refinement is due to the presence of the monadic Barcan formula, which requires that the selected frame satisfies not only the left but also the right commutativity condition. Due to this, the procedure may not terminate in finitely many steps (closing under left commutativity necessitates closing under right commutatvity and vice-versa; thus, these two processes alternate and trigger each other). Therefore, the selected frame $\widehat {\mathfrak {F}}$ will be countable, but not necessarily finite. However, the frame will be an $\mathbf{MGrzB}$ -frame with a uniform bound on its depth.

While our construction can be performed in any descriptive frame, it is sufficient to only work with canonical models (see, e.g., [Reference Chagrov and Zakharyaschev7, Section 5.1]).

We will now restrict our attention to $\mathbf{MGrzB}$ and its extensions. For any extension $\mathbf {M}$ of $\mathbf {MGrzB}$ , let $\mathfrak {M}_{\mathbf {M}} :=(\mathfrak {F}_{\mathbf {M}}, v_{\mathbf {M}})$ be the canonical model of $\mathbf{M}$ , where $\mathfrak {F}_{\mathbf {M}} :=(X_{\mathbf {M}}, R_{\mathbf {M}}, E_{\mathbf {M}})$ is the canonical frame and $v_{\mathbf {M}}$ is the canonical valuation.

Let $U\subseteq X_{\mathbf {M}}$ . We recall (see, e.g., [Reference Esakia, Bezhanishvili and Holliday9, Definition 1.4.9]) that $x \in U$ is a maximal point of U provided $x\mathrel {R_{\mathbf {M}}}y$ implies $x=y$ for all $y\in U$ . Let ${\mathbf {max}}\hspace {2pt}U$ denote the set of maximal points of U. It follows from the well-known Fine–Esakia principle (see, e.g., [Reference Esakia, Bezhanishvili and Holliday9, Corollary 3.5.7]) that for each definable subset $U\subseteq X_{\mathbf {M}}$ and $x\in U$ , we have $R_{\mathbf {M}}[x]\cap \mathbf {max}\hspace {2pt}U \neq \varnothing $ . In particular, it is not possible to “exit” U via $R_{\mathbf {M}}$ from a maximal point and re-enter it.

We will work with the stronger notion of maximality, introduced in [Reference Bezhanishvili and Khan6]. To define strong maximality, let $Q_{\mathbf {M}}$ be the composition of $R_{\mathbf {M}}$ and $E_{\mathbf {M}}$ ; that is,

$$ \begin{align*} x \mathrel{Q_{\mathbf{M}}} y\iff (\exists z\in X_{\mathbf{M}})(x \mathrel{R_{\mathbf{M}}} z \text{ and } z\mathrel{E_{\mathbf{M}}} y). \end{align*} $$

Clearly $R_{\mathbf {M}}\subseteq Q_{\mathbf {M}}$ , but this inclusion is in general strict. We will refer to the elements of $Q_{\mathbf {M}} \setminus R_{\mathbf {M}}$ as proper Q-relations (see Remarks 4.9 and 4.14).

Definition 4.3 [Reference Bezhanishvili and Khan6, Definition 6.13].

Let $U\subseteq X_{\mathbf {M}}$ . We call $x\in \mathbf {max}\hspace {2pt}U$ a strongly maximal point of U if for any $y\in X_{\mathbf {M}}$ ,

$$ \begin{align*} x\mathrel{Q_{\mathbf{M}}}y \text{ and } y\in U \implies x\mathrel{E_{\mathbf{M}}}y. \end{align*} $$

We let ${\mathbf {smax}}\hspace {2pt}U$ denote the set of strongly maximal points of U.

The following, taken from [Reference Bezhanishvili and Khan6, Remark 6.14], is an illustrative example highlighting the difference between maximal and strongly maximal points.

Example 4.4. Consider the finite frame $\mathfrak {F}=(X,R,E)$ shown below, where R is represented by the arrows (indicating non-reflexive relations) and circles (indicating reflexive relations), and the E-clusters are depicted in blue. Since X is finite, there exists a valuation $v$ under which every subset of X is definable. Let $U=\{a,b,c\}$ (the dotted red curve on the diagram). Clearly $a\in \mathbf {max}\hspace {2pt}U$ , but $a\notin \mathbf {smax}\hspace {2pt}U$ since $a\mathrel {Q}c$ , $c\in U$ , and .

While the notions of maximality and strong maximality differ in general, they agree for E-saturated definable subsets, where we recall that a subset V is E-saturated provided $x \in V$ and $x \mathrel {E} y$ imply $y \in V$ . Indeed, for such a definable subset V, we have $\mathbf {smax}\hspace {2pt}V =\mathbf {max}\hspace {2pt}V$ (see [Reference Bezhanishvili and Khan6, Proposition 6.15]). It is worth pointing out that the set U in the example above is not E-saturated.

We will utilize the following feature of strongly maximal points, which is crucial for our construction.

Consider $\mathfrak {M}_{\mathbf {M}}=(\mathfrak {F}_{\mathbf {M}},v_{\mathbf {M}})$ . Since the monadic Barcan formula and its converse are Sahlqvist, they are canonical (see, e.g., [Reference Gabbay, Kurucz, Wolter and Zakharyaschev12, p. 223]). Thus, the frame $\mathfrak {F}_{\mathbf {M}}$ satisfies both left and right commutativity.

Let $\mathfrak {M}_{\mathbf {M}} \not \models \varphi $ and let S be the set of subformulae of $\varphi $ . We will iteratively construct a new model $\widehat {\mathfrak {M}}$ such that $\widehat {\mathfrak {M}}\not \models \varphi $ . By Theorem 4.5(1), there is $x\in \mathbf {smax}\hspace {2pt}v_{\mathbf {M}}(\neg \varphi )$ . To initiate the construction of the model $\widehat {\mathfrak {M}}$ , we “select” x, label it $\widehat {x}$ , and proceed by selecting additional points. For $t\in X_{\mathbf {M}}$ , we label a selected copy by $\widehat {t}$ . New points in the selected model are introduced either as “witnesses” of formulae in S of the form $\exists \psi ,\Diamond \psi $ or as “witnesses” of left or right commutativity.

Define

$$ \begin{align*} W_t^\exists=\{\exists\psi\in S &\mid \mathfrak{M}_{\mathbf{M}},t\models\exists\psi \text{ but } \mathfrak{M}_{\mathbf{M}},t\not\models\psi\},\\ W_t^\Diamond=\{\Diamond\psi\in S &\mid \mathfrak{M}_{\mathbf{M}},t\models\Diamond\psi \text{ but } \mathfrak{M}_{\mathbf{M}},t\not\models\psi\}. \end{align*} $$

The sets $W_t^\exists $ and $W_t^\Diamond $ let us keep track of the subformulae of $\varphi $ that demand the addition of a new witness from a point $\widehat {t}$ in the model $\widehat {\mathfrak {M}}$ . A point added to satisfy a subformula of the form $\exists \psi $ will be called an $\exists $ -witness, and a point added to satisfy a subformula of the form $\Diamond \psi $ a $\Diamond $ -witness.

We will drop the subscripts from $\mathfrak {M}_{\mathbf {M}}=(\mathfrak {F}_{\mathbf {M}},v_{\mathbf {M}})$ and $\mathfrak {F}_{\mathbf {M}}=(X_{\mathbf {M}},R_{\mathbf {M}}, E_{\mathbf {M}})$ , and simply write $t\models \psi $ to indicate $\mathfrak {M},t\models \psi $ . In doing so, no ambiguity will arise since statements about the model $\widehat {\mathfrak {M}}$ will be clearly indicated by the use of hats.

Define the equivalence relation $\sim _S$ by

$$ \begin{align*} x\sim_S y\iff x\models \psi \text{ iff } y\models \psi \text{ for any } \psi\in S. \end{align*} $$

1. (1) Initial step: Select $x\in \mathbf {smax}\hspace {2pt}v(\neg \varphi )$ and let

   $$ \begin{align*} X_0=\{\widehat{x}\}, R_0=X_0^2, E_0=X_0^2. \end{align*} $$

   Set $\mathfrak {F}_0=(X_0,R_0,E_0)$ and note that $\mathfrak {F}_0$ is a partially ordered $\mathbf {MKB}$ -frame.

   Suppose a $(\mathbf {Grz}\otimes \mathbf {S5})$ -frame $\mathfrak {F}_{k-1}=(X_{k-1},R_{k-1},E_{k-1})$ has already been constructed by taking copies of strongly maximal points in $\mathfrak {F}$ , and satisfying the desiderata supplied by Lemma 4.17. We describe the construction of a $(\mathbf {Grz}\otimes \mathbf {S5})$ -frame $\mathfrak {F}_k=(X_k,R_k,E_k)$ extending $\mathfrak {F}_{k-1}$ .

2. (2) $\exists $ Step: Selecting $\exists $ -witnesses. Set $X_k^\exists =X_{k-1}, R_k^\exists =R_{k-1}, E_k^\exists =E_{k-1}$ .

   Suppose $\widehat {t}\in X_{k-1}$ and $\exists \psi \in W_t^\exists $ . If there is already some $\widehat {u}\in X_k^\exists $ such that $\widehat {t}\mathrel {E_k^\exists }\widehat {u}$ and $u\models \psi $ , there is nothing to do. Otherwise, we choose a witness using the following lemma.

   Lemma 4.6 [Reference Bezhanishvili and Khan6, Lemma 7.2].

   Let $z\in {\mathbf {smax}}\hspace {2pt}U$ for some definable subset U. If $\exists \psi \in W_z^{\exists }$ , then there is $y \in {\mathbf {smax}}\hspace {2pt}(E[U]\cap v(\psi ))$ such that $y \mathrel {E} z$ .

   Since $\widehat {t}\in X_{k-1}$ , and we only select strongly maximal points at each stage of the construction, it follows that $t\in \mathbf {smax}\hspace {2pt} U$ for some definable subset U. Therefore, by Lemma 4.6, there is $w\in \mathbf {smax}\hspace {2pt}(E[U]\cap v(\psi ))$ such that $w\mathrel {E}t$ (in particular, note that $w\models \psi $ and that $E[U]\cap v(\psi )$ is definable). Add $\widehat {w}$ to $X_k^\exists $ , add $(\widehat {t},\widehat {w})$ to $E_k^\exists $ and generate the least equivalence relation. Add $(\widehat {w},\widehat {w})$ to $R_k^\exists $ . Repeat this process until all points in $X_{k-1}$ have witnesses for subformulae of the form $\exists \psi $ .

3. (3) $\Diamond $ Step: Selecting $\Diamond $ -witnesses. Set $X_k^\Diamond =X_k^\exists , R_k^\Diamond =R_k^\exists , E_k^\Diamond =E_k^\exists $ .

   Suppose $\widehat {y}\in X_k^\exists $ and $\Diamond \psi \in W_y^\Diamond $ . If there is already some $\widehat {z}\in X_k^\Diamond $ such that $\widehat {y}\mathrel {R_k^\Diamond } \widehat {z}$ and $z\models \psi $ , there is nothing to do. Otherwise, we use the following lemma to find a witness.

   Lemma 4.7 [Reference Bezhanishvili and Khan6, Lemma 7.3].

   For $\Diamond \psi \in W_y^{\Diamond }$ let

   $$ \begin{align*} A = v(\Diamond\psi)\cap\bigcap\big\{ v(\neg\Diamond\alpha)\mid \Diamond\alpha\in S,\, y\not\models \Diamond\alpha \big\}. \end{align*} $$

   Then there is $z\in X$ such that the following conditions are satisfied:

   1. (1) $y\mathrel {Q}z$ , $z\neq y$ , and $z\in \mathbf {smax}\hspace {2pt}A\cap \mathbf {max}\hspace {2pt}v(\psi )$ .

   2. (2) $y\not \models \Diamond \alpha $ implies $z\not \models \alpha $ for each $\Diamond \alpha \in S$ .

   3. (3) If $y\mathrel {E}z$ , then there is $u\in {\mathbf {smax}}\hspace {2pt}A \cap {\mathbf {max}}\hspace {2pt}v(\psi )$ such that $y\mathrel {R}u$ and $u\mathrel {E}y$ .

   4. (4) If $z\mathrel {Q}t$ and , then for all t.

   Horizontal step: Selecting $\Diamond $ -witnesses in E-clusters.We will select points u satisfying
   (H) $$ \begin{align} y\mathrel{R}u, y\mathrel{E}u, \text{ and } u\in\mathbf{smax}\hspace{2pt} A\cap\mathbf{max}\hspace{2pt} v(\psi). \end{align} $$

   1. (h1) Suppose there is already some $\widehat {u}\in X_k^\Diamond $ such that (H) holds for u.

   2. (h2) Then add $(\widehat {y},\widehat {u})$ to $R_k^\Diamond $ and take the reflexive–transitive closure. Further, add $(\widehat {y},\widehat {u})$ to $E_k^\Diamond $ and generate the least equivalence relation.

   3. (h3) If there is no such $\widehat {u}$ , then by Lemma 4.7(1) there is some $z\in \mathbf {smax}\hspace {2pt}A\cap \mathbf {max}\hspace {2pt}v(\psi )$ such that $y\mathrel {Q}z$ . If additionally we have $y\mathrel {E}z$ , then by Lemma 4.7(3) there is u satisfying (H). We add $\widehat {u}$ to $X_k^\Diamond $ and introduce relations as in (h2).

   Repeat the above steps until all such $\Diamond $ -witnesses for $\widehat {y}$ from $E[y]$ are added. Proceed to the next step.

   Remark 4.8. This is the only step in the construction where a “horizontal” $R_k^\Diamond $ -arrow is drawn, that is, relations of the form $\widehat {y}\mathrel {R_k^\Diamond }\widehat {u}$ and $\widehat {y}\mathrel {E_k^\Diamond }\widehat {u}$ are introduced. Adding such horizontal arrows will not be required when dealing with $\mathbf {M}^+\mathbf {GrzB}$ and $\mathbf {MGLB}$ since our selection process for these systems only produces clean clusters (see Theorems 5.5 and 5.10).

   Vertical step: Selecting $\Diamond $ -witnesses outside E-clusters.We will select points z satisfying
   (V)

   

   1. (v1) Suppose there is already some $\widehat {z}\in X_k^\Diamond $ such that (V) holds for z. Then add $(\widehat {y},\widehat {z})$ to $R_k^\Diamond $ and take the reflexive–transitive closure.

   2. (v2) If there is no such $\widehat {z}$ , then by Lemma 4.7(1) there is some $z\in \mathbf {smax}\hspace {2pt}A\cap \mathbf {max}\hspace {2pt}v(\psi )$ such that $y\mathrel {Q}z$ . Without loss of generality we may assume that since the case $y\mathrel {E}z$ is already considered in the horizontal step. Clearly z satisfies (V). We add $\widehat {z}$ to $X_k^\Diamond $ , add $(\widehat {y},\widehat {z})$ to $R_k^\Diamond $ and take the reflexive–transitive closure, and add $(\widehat {z},\widehat {z})$ to $E_k^\Diamond $ .

   3. (v3) If $z\mathrel {E}t$ and $\widehat {t}$ has been previously introduced, then add $(\widehat {z},\widehat {t})$ to $E_k^\Diamond $ and generate the least equivalence relation.

   Repeat the above steps until all $\Diamond $ -witnesses for $\widehat {y}$ occurring outside $E[y]$ are added. Repeat the horizontal and vertical steps for all points in $X_k^\exists $ .

   Remark 4.9. The vertical step may involve turning a proper Q-arrow into an $R_k^\Diamond $ -arrow. This will be one of the two instances where this occurs (for the other instance, see Remark 4.14).

   Lemma 4.10 [Reference Bezhanishvili and Khan6, Lemma 7.4].

   For $\widehat {u},\widehat {w}\in X_k^\Diamond $ ,

   1. (a) $\widehat {u}\mathrel {E_k^\Diamond }\widehat {w}$ iff $u\mathrel {E}w$ ;

   2. (b) $\widehat {u}\mathrel {R_k^\Diamond }\widehat {w}$ implies $u\mathrel {Q}w$ .

4. (4) Commutativity step: In this final step, we close the selected points under left and right commutativity.

   1. (LC) Left commutativity: Set $X_k^L=X_k^\Diamond , R_k^L=R_k^\Diamond , E_k^L=E_k^\Diamond $ . Suppose $\widehat {t}\mathrel {E_k^{\Diamond }}\widehat {u}$ and $\widehat {u}\mathrel {R_k^{\Diamond }}\widehat {w}$ . We need to find some $\widehat {s}$ such that $\widehat {t}\mathrel {R_k^L}\widehat {s}$ and $\widehat {s}\mathrel {E_k^L}\widehat {w}$ . In case $\widehat {u}\mathrel {E_k^{\Diamond }}\widehat {w}$ , the choice of $\widehat {s}$ is trivial since we can simply take $\widehat {s}=\widehat {t}$ . Hence, suppose . Then we can find $\widehat {s}$ using the following.

      Lemma 4.11 [Reference Bezhanishvili and Khan6, Lemma 7.5].

      Let $t\mathrel {Q}w$ and $w\in \mathbf {smax}\hspace {2pt}U$ for some definable set U. Then there exists $s\in \mathbf {smax}\hspace {2pt}E[U]$ such that $t\mathrel {R}s$ and $s\mathrel {E}w$ .

      Since $\widehat {t}\mathrel {E_k^{\Diamond }}\widehat {u}$ and $\widehat {u}\mathrel {R_k^{\Diamond }}\widehat {w}$ , Lemma 4.10 gives that $t\mathrel {E}u$ and $u\mathrel {Q}w$ . Thus, $t\mathrel {Q}w$ , where $w\in \mathbf {smax}\hspace {2pt}U$ for some definable subset U (since every selected point is strongly maximal in some definable subset). Therefore, Lemma 4.11 applies, by which there is $s\in \mathbf {smax}\hspace {2pt}E[U]$ such that $t\mathrel {R}s$ and $s\mathrel {E}w$ .

      If $\widehat {s}$ is not already present, add it to $X_k^L$ . Also add $(\widehat {t},\widehat {s})$ to $R_k^L$ and take the reflexive–transitive closure. In addition, add $(\widehat {s},\widehat {w})$ to $E_k^L$ and generate the least equivalence relation. Repeat this process for every instance of $\widehat {t}\mathrel {E_k^{\Diamond }}\widehat {u}$ and $\widehat {u}\mathrel {R_k^{\Diamond }}\widehat {w}$ until left commutativity is satisfied for all the points in $X_k^{\Diamond }$ . We have the following analog of Lemma 4.10, the proof of which is similar to that of [Reference Bezhanishvili and Khan6, Lemma 4.6].

      Lemma 4.12. For $\widehat {u},\widehat {w}\in X_k^L$ ,

      1. (1) $\widehat {u}\mathrel {E_k^L}\widehat {w}$ iff $u\mathrel {E}w$ ;

      2. (2) $\widehat {u}\mathrel {R_k^L}\widehat {w}$ implies $u\mathrel {Q}w$ .

      Proof. (1) The implication $\widehat {u}\mathrel {E_k^L}\widehat {w}\implies u\mathrel {E}w$ is clear since we introduce $E_k^L$ -relations between points only if their original copies are E-related. Conversely, suppose $u\mathrel {E}w$ . Since $\widehat {u},\widehat {w}\in X_k^L$ , there are $\widehat {t}, \widehat {s}\in X_k^{\Diamond }$ such that $\widehat {w}\mathrel {E_k^L}\widehat {t}$ and $\widehat {u}\mathrel {E_k^L}\widehat {s}$ (because each point that may be introduced via (LC) must involve creating an $E_k^L$ -relation for left commutativity). Thus, by the forward implication, $t\mathrel {E}w$ and $u\mathrel {E}s$ , and hence $t\mathrel {E}s$ . By Lemma 4.10, we deduce that $\widehat {s}\mathrel {E_k^{\Diamond }}\widehat {t}$ , and so $\widehat {t}\mathrel {E_k^L}\widehat {s}$ . Thus, $\widehat {u}\mathrel {E_k^L}\widehat {w}$ .

      (2) This is immediate since an $R_k^L$ -relation is introduced between points only if their original copies are Q-related.

   1. (RC) Right commutativity: Set $X_k^R=X_k^{L}, R_k^R=R_k^{L}, E_k^R=E_k^{L}$ . Suppose $\widehat {t}\mathrel {R_k^L}\widehat {w}$ and $\widehat {w}\mathrel {E_k^L}\widehat {u}$ . We need to find $\widehat {s}$ such that $\widehat {t}\mathrel {E_k^R}\widehat {s}$ and $\widehat {s}\mathrel {R_k^R}\widehat {u}$ . If $\widehat {t}\mathrel {E_k^L}\widehat {w}$ , there is nothing to do since we can take $\widehat {s}=\widehat {u}$ . Hence, suppose that . We will find $\widehat {s}$ using the following.

      Lemma 4.13. Let $t\in \mathbf {smax}\hspace {2pt}U$ for some definable set U. If $t\mathrel {Q}u$ , then there is $s\in \mathbf {smax}\hspace {2pt}(E[U]\cap V)$ such that $s\mathrel {Q}u$ and $s\mathrel {E}t$ , where

      $$ \begin{align*} V=\bigcap\{v(\Diamond\psi)\mid \Diamond\psi\in S, u\models\Diamond\psi\}. \end{align*} $$

      Proof. Since $t\mathrel {Q}u$ , there is a with $t\mathrel {R}a$ and $a\mathrel {E}u$ . Because $\mathfrak {F}$ satisfies right commutativity, there is b with $t\mathrel {E}b$ and $b\mathrel {R}u$ . The above intersection defining V is finite, and thus V is a definable set. Moreover, due to transitivity, $b\in V \cap E[U]$ and $E[U]\cap V$ is a definable set. By Theorem 4.5(1), we can choose $s\in Q[b]\cap \mathbf {smax}\hspace {2pt}(E[U]\cap V)$ . We claim that s is the desired point. We first show that $s\mathrel {E}t$ . Because $t\mathrel {E}b$ and $b\mathrel {Q}s$ , we have $t\mathrel {Q}s$ . Since $s\in E[U]$ , there is $c \in U$ with $c\mathrel {E}s$ . Therefore, $t\mathrel {Q}c$ and $c\in U$ . Because $t\in \mathbf {smax}\hspace {2pt}U$ , we must have $c\mathrel {E}t$ , which yields $s\mathrel {E}t$ . Now observe that $t\mathrel {Q}u$ and $s\mathrel {E}t$ . Thus, $s\mathrel {Q}u$ , concluding the proof.

      Since $\widehat {t}\mathrel {R_k^{L}}\widehat {w}$ and $\widehat {w}\mathrel {E_k^{L}}\widehat {u}$ , we have $t\mathrel {Q}w$ and $w\mathrel {E}u$ by Lemma 4.12. This yields ${t\mathrel {Q}u}$ , and by construction, $t\in \mathbf {smax}\hspace {2pt}U$ for some definable subset U. By Lemma 4.13, there exists ${s\in \mathbf {smax}\hspace {2pt}(E[U]\cap V)}$ with $s\mathrel {Q}u$ and $s\mathrel {E}t$ , where V is defined as above.

      If $\widehat {s}$ is not already there, add $\widehat {s}$ to $X_k^R$ . Also, add $(\widehat {s},\widehat {u})$ to $R_k^R$ and take the reflexive–transitive closure, and add $(\widehat {t},\widehat {s})$ to $E_k^R$ and generate the least equivalence relation. Repeat until right commutativity is satisfied for all the points in $X_k^{L}$ .

      Remark 4.14. In this step, a proper Q-arrow may be turned into an $R_k^R$ -arrow. This is the second instance in the construction where this occurs (see Remark 4.9 for the first instance).

      Lemma 4.15. For $\widehat {u},\widehat {w}\in X_k^R$ ,

      1. (i) $\widehat {u}\mathrel {E_k^R}\widehat {w}$ iff $u\mathrel {E}w$ ;

      2. (ii) $\widehat {u}\mathrel {R_k^R}\widehat {w}$ implies $u\mathrel {Q}w$ .

      Proof. The proof is analogous to that of Lemma 4.12, but uses Lemma 4.12 instead of Lemma 4.10.

Set

$$ \begin{align*} X_k=X_k^R, \quad R_k=R_k^R, \quad E_k=E_k^R, \end{align*} $$

and let $\mathfrak {F}_k=(X_k,R_k,E_k)$ .

For the reader’s convenience, we depict the various stages of the construction in the diagram below. As usual, circles indicate reflexive points, arrows represent non-reflexive relations in $R_k$ , and $E_k$ -clusters are in blue. At each stage, the newly added arrows and points are shown in red, while the arrows and points added in the preceding steps are gray and black, respectively.

The following is a weakened version of [Reference Bezhanishvili and Khan6, Lemma 7.8]. In particular, the frame constructed in [Reference Bezhanishvili and Khan6, Lemma 7.8] is a finite $\mathbf {MGrz}$ -frame, while the frame produced by the modified construction is neither left nor right commutative.

Now, define $\widehat {\mathfrak {F}}=(\widehat {X},\widehat {R},\widehat {E})$ by setting

$$ \begin{align*} \widehat{X}=\bigcup_{k<\omega}X_k, \quad \widehat{R}=\bigcup_{k<\omega}R_k, \quad \widehat{E}=\bigcup_{k<\omega}E_k. \end{align*} $$

As a consequence of Lemma 4.18, we obtain the following lemma.

To obtain a model based on $\widehat {\mathfrak {F}}$ , we define a valuation $\widehat {v}$ on $\widehat {\mathfrak {F}}$ by setting

$$ \begin{align*}\widehat{v}(p)=\{\widehat{t}\in\widehat{X}\mid t\in v(p)\}\end{align*} $$

for $p\in S$ and $v(p)=\varnothing $ otherwise. We abbreviate satisfaction $\widehat {\mathfrak {M}},\widehat {t}\models \psi $ in the model $\widehat {\mathfrak {M}}=(\widehat {\mathfrak {F}},\widehat {v})$ by $\widehat {t}\models \psi $ .

Lemma 4.20 (Truth lemma).

For any $\widehat {t}\in \widehat {X}$ and $\psi \in S$ ,

$$ \begin{align*} \widehat{t}\models\psi \iff t\models\psi. \end{align*} $$

Proof. The proof is by induction on the complexity of $\psi $ . The base step is clear by the definition of $\widehat {v}$ . By the induction hypothesis, the claim is clearly true when $\psi $ is a Boolean combination of subformulae. We only need to show the above when $\psi =\exists \delta $ or $\psi =\Diamond \delta $ .

Suppose $t\models \exists \delta $ . If $t\models \delta $ , then $\widehat {t}\models \delta $ by the induction hypothesis, and so $\widehat {t}\mathrel {\widehat {E}}\widehat {t}$ implies $\widehat {t}\models \exists \delta $ . Suppose $t\not \models \delta $ . Then $\exists \delta \in W_t^\exists $ , and there is a least $k<\omega $ for which $\widehat {t}\in X_k$ . Hence, by construction, there is $\widehat {z}\in X_{k+1}$ such that $\widehat {t}\mathrel {E_{k+1}}\widehat {z}$ and $z\models \delta $ . By the induction hypothesis, $\widehat {z}\models \delta $ . Since $E_{k+1}\subseteq \widehat {E}$ , we have $\widehat {t}\mathrel {\widehat {E}}\widehat {z}$ and $\widehat {z}\models \delta $ . Thus, $\widehat {t}\models \exists \delta $ .

Conversely, suppose $\widehat {t}\models \exists \delta $ . Then there is $\widehat {z}\in \widehat {X}$ such that $\widehat {t}\mathrel {\widehat {E}}\widehat {z}$ and $\widehat {z}\models \delta $ . Take the least $k<\omega $ such that $\widehat {t}\mathrel {E_k}\widehat {z}$ . By Lemma 4.17(1), $y\mathrel {E}z$ , and by the induction hypothesis, $z\models \delta $ . Hence, $y\models \exists \delta $ .

Next suppose $t\models \Diamond \delta $ . The proof is similar to the case when $t\models \exists \delta $ . In particular, if $t\models \delta $ , then $\widehat {t}\models \delta $ by the induction hypothesis, implying that $\widehat {t}\models \Diamond \delta $ since $\widehat {t}\mathrel {\widehat {R}}\widehat {t}$ . Suppose $t\not \models \delta $ . Then $\Diamond \delta \in W_t^\Diamond $ , and there is a least $k<\omega $ such that $\widehat {t}\in X_k$ . By construction, there is $\widehat {z}\in X_{k+1}$ such that $\widehat {t}\mathrel {R_{k+1}}\widehat {z}$ and $z\models \delta $ . The induction hypothesis implies that $\widehat {z}\models \delta $ . Since $R_{k+1}\subseteq \widehat {R}$ , we have $\widehat {t}\mathrel {\widehat {R}}\widehat {z}$ and $\widehat {z}\models \delta $ . Thus, $\widehat {t}\models \Diamond \delta $ .

Conversely, suppose $\widehat {t}\models \Diamond \delta $ . Then there is $\widehat {z}\in \widehat {X}$ such that $\widehat {t}\mathrel {\widehat {R}}\widehat {z}$ and $\widehat {z}\models \delta $ . Choose the least $k<\omega $ such that $\widehat {t}\mathrel {R_k}\widehat {z}$ . Because we take the reflexive–transitive closure at each step, we have a chain

$$ \begin{align*}\widehat{t}=\widehat{x}_1\mathrel{R_k}\widehat{x}_2\mathrel{R_k}\dots\mathrel{R_k}\widehat{x}_n\mathrel{R_k}\widehat{x}_{n+1}=\widehat{z},\end{align*} $$

where the relation $(\widehat {x}_j,\widehat {x}_{j+1})$ is introduced to $R_k$ during the course of the construction. To see that $t\models \Diamond \delta $ , we first show the following.

Claim 4.21. For any $j\geq 2$ , we have $x_j\models \Diamond \delta \implies x_{j-1}\models \Diamond \delta $ .

Proof of the claim.

Suppose $x_j\models \Diamond \delta $ . If $x_{j-1}\mathrel {R}x_j$ , then $x_{j-1}\models \Diamond \Diamond \delta $ , which yields $x_{j-1}\models \Diamond \delta $ . Suppose . By Lemma 4.17(2), $x_{j-1}\mathrel {Q}x_j$ . Since ${x_{j-1}\mathrel {Q}x_j}$ , , and $\widehat {x}_{j-1}\mathrel {R_k}\widehat {x}_j$ , a proper Q-arrow was turned into a $R_k$ -arrow. This happens in only two stages of the construction: either in the vertical step to introduce $\Diamond $ -witnesses or in the commutativity step (RC) (see Remarks 4.9 and 4.14). We handle each case separately.

1. (1) Suppose $\widehat {x}_{j-1}\mathrel {R_k}\widehat {x}_j$ was introduced to add $\widehat {x}_j$ as a vertical $\Diamond $ -witness for $\widehat {x}_{j-1}$ with respect to some $\Diamond \psi \in S$ . Then by (V), we must have $x_j\in \mathbf {smax}\hspace {2pt}A$ , where

   $$ \begin{align*} A = v(\Diamond\psi)\cap\bigcap\big\{ v(\neg\Diamond\alpha)\mid \Diamond\alpha\in S,\, x_{j-1}\not\models \Diamond\alpha \big\}. \end{align*} $$
   Hence, if $x_{j-1}\not \models \Diamond \delta $ , we must have $x_j\not \models \Diamond \delta $ , which contradicts our assumption that $x_j\models \Diamond \delta $ . Therefore, $x_{j-1}\models \Diamond \delta $ .

2. (2) Suppose $\widehat {x}_{j-1}\mathrel {R_k}\widehat {x}_j$ was introduced to close under right commutativity. Then (RC) together with Lemma 4.13 implies that $x_{j-1}\in V$ , where

   $$ \begin{align*} V=\bigcap\{v(\Diamond\psi)\mid \Diamond\psi\in S, x_j\models\Diamond\psi\}. \end{align*} $$
   Thus, since $x_j\models \Diamond \delta $ , we have $x_{j-1}\models \Diamond \delta $ .

Now, applying Lemma 4.17(4) to $\widehat {x}_{n+1}=\widehat {z}$ yields $x_{n+1}=z$ , and by induction hypothesis we have ${z}\models \delta $ . Thus, $x_{n+1}\models \delta $ , and by the repeated application of $x_j\models \Diamond \delta \implies x_{j-1}\models \Diamond \delta $ , we obtain $x_1\models \Diamond \delta $ . From $\widehat {x}_1=\widehat {t}$ it follows that $x_1=t$ by Lemma 4.17(4), and hence $t \models \Diamond \delta $ .

We next show that $\widehat {\mathfrak {F}}=(\widehat {X},\widehat {R},\widehat {E})$ has bounded depth. For this we require working with the quotient of $\widehat {\mathfrak {F}}$ by the equivalence relation $\widehat {E}$ . This generalizes the well-studied notion of a skeleton in modal logic (see, e.g., [Reference Chagrov and Zakharyaschev7, p. 68]). The skeleta of the above form were first considered in the setting of monadic intuitionistic logics (see, e.g., [Reference Bezhanishvili2, Reference Suzuki24]), and were appropriately redefined for mm-logics in [Reference Bezhanishvili, Brantley and Ilin4–Reference Bezhanishvili and Khan6].

Definition 4.22. The E-skeleton of a $(\mathbf {K}\otimes \mathbf {S5})$ -frame $\mathfrak {F}=(X,R,E)$ is the frame $\mathfrak {F}_0=(X_0,R_0)$ , where $X_0$ is the quotient of X by E. We denote elements of $X_0$ by $[x]$ , where $x\in X$ , and define

$$ \begin{align*} [x]\mathrel{R_0}[y]\iff x'\mathrel{R}y' \text{ for some } x' \in [x] \text{ and } y' \in [y]. \end{align*} $$

Remark 4.23. When $\mathfrak {F}$ is an $\mathbf {MK}$ -frame, the relation $R_0$ can be defined simply by taking

$$ \begin{align*} [x]\mathrel{R_0}[y]\iff x\mathrel{Q}y. \end{align*} $$

Indeed, it follows from the definition of Q that ${x\mathrel {Q}y}$ implies $[x]\mathrel {R}_0[y]$ . Conversely, let $[x]\mathrel {R}_0[y]$ . Then $x'\mathrel {R}y'$ for some ${x' \in [x]} \text { and } {y' \in [y]}$ . Therefore, $x\mathrel {E}x'$ , $x'\mathrel {R}y'$ , and $y'\mathrel {E}y$ . Thus, left commutativity implies that $x\mathrel {Q}y$ .

In general, for a $(\mathbf {K}\otimes \mathbf {S5})$ -frame $\mathfrak {F}=(X,R,E)$ , the E-skeleton $\mathfrak {F}_0=(X_0,R_0)$ is neither reflexive nor transitive. However, we show that the E-skeleton of $\widehat {\mathfrak {F}}$ is indeed a poset. We will also work with the E-skeleta of the intermediate frames $\mathfrak {F}_k$ . For a point $\widehat {u}$ in $\mathfrak {F}_k$ , we sometimes need to distinguish between the point $[\widehat {u}]$ in $(\mathfrak {F}_k)_0$ and the point $[\widehat {u}]$ in $\widehat {\mathfrak {F}}_0$ (since these points arise from different equivalence relations). Whenever such a distinction is necessary, we write $[\widehat {u}]_k$ for the corresponding point in $(\mathfrak {F}_k)_0$ .

We recall (see, e.g., [Reference Chagrov and Zakharyaschev7, p. 362]) that a frame $\mathfrak {F}=(X,R)$ is acyclic if for any distinct $x_1,x_2,\ldots \in X$ with $x_1\mathrel {R}x_2\mathrel {R}\dots $ we have for $j>i$ (observe that each acyclic frame is antisymmetric).

To see that $\widehat {\mathfrak {F}}$ has bounded depth, observe that the projection map $\pi \colon \widehat {\mathfrak {F}}\to \widehat {\mathfrak {F}}_0$ , given by $\widehat {x}\mapsto [\widehat {x}]$ , collapses each chain C in $\widehat {\mathfrak {F}}$ to a chain $C_0$ in $\widehat {\mathfrak {F}}_0$ . Thus, to see that the depth of each chain C is bounded, it is enough to show that $\widehat {\mathfrak {F}}_0$ has bounded depth, and that the size of each set $\pi ^{-1}[\widehat {y}]\cap C$ is uniformly bounded for each $[\widehat {y}]$ in $C_0$ .

The proof of the following result is similar to [Reference Bezhanishvili and Khan6, Lemma 7.12]. The key difference is that the proof in [Reference Bezhanishvili and Khan6, Lemma 7.12] leverages the E-skeleta of the intermediate frames $\mathfrak {F}_k$ , which are left commutative, while the frames $\mathfrak {F}_k$ in the present construction are not.

Lemma 4.26. If $\widehat {C}$ is a strict $\widehat {R}_0$ -chain

$$\begin{align*}[\widehat{y}_0]\mathrel{\widehat{R}_0}[\widehat{y}_1]\dots [\widehat{y}_{n-1}]\mathrel{\widehat{R}_0}[\widehat{y}_n]\dots\end{align*}$$

in $\widehat {\mathfrak {F}}_0=(\widehat {X}_0, \widehat {R}_0)$ , then the length of $\widehat {C}$ is bounded by $2^{|S|+1}$ .

Proof. From $[\widehat {y}_i]\mathrel {\widehat {R}_0}[\widehat {y}_{i+1}]$ it follows that $\widehat {y}_i\mathrel {\widehat {Q}}\widehat {y}_{i+1}$ and (otherwise $[\widehat {y}_i] = [\widehat {y}_{i+1}]$ , contradicting that we have a strict chain). Let $k<\omega $ be the least number for which $\widehat {y}_i\mathrel {Q_k}\widehat {y}_{i+1}$ . From it follows that . Thus, ${\widehat {y}_i\mathrel {R_k}\widehat {t}}$ , $\widehat {t}\mathrel {E_k}\widehat {y}_{i+1}$ , and . In other words, we have ${[\widehat {y}_i]_k\mathrel {(R_k)_0}[\widehat {y}_{i+1}]_k}$ and ${[\widehat {y}_i]_k\neq [\widehat {y}_{i+1}]_k}$ in $(\mathfrak {F}_k)_0$ . Since $\mathfrak {F}_k$ is finite, $(\mathfrak {F}_k)_0$ is finite. Therefore, we may assume that $[\widehat {y}_{i+1}]_k$ is an immediate successor of $[\widehat {y}_i]_k$ in $(\mathfrak {F}_k)_0$ for otherwise we can decompose $[\widehat {y}_i]_k\mathrel {(R_k)_0}[\widehat {y}_{i+1}]_k$ further as ${[\widehat {y}_i]_k\mathrel {(R_k)_0}[\widehat {t}_1]_k\dots [\widehat {t}_{n-1}]_k\mathrel {(R_k)_0}[\widehat {t}_n]_k=[\widehat {y}_{i+1}]_k}$ , where each $[\widehat {t}_i]_k$ is indeed an immediate successor. Thus, by Lemma 4.24(2), we can extend $\widehat {C}$ to a longer chain by including the points $[\widehat {t}_1],\dots ,[\widehat {t}_{n-1}]$ .

Since immediate successors in $(\mathfrak {F}_k)_0$ are determined by $R_k^\Diamond $ -arrows drawn to introduce vertical $\Diamond $ -witnesses, there must be $\widehat {y}\in [\widehat {y}_i]_k$ , $\widehat {z}\in [\widehat {y}_{i+1}]_k$ , and $\Diamond \psi \in W_y^\Diamond $ such that $\widehat {z}$ is a vertical $\Diamond $ -witness for $\widehat {y}$ with respect to $\Diamond \psi $ . Because $\widehat {y}\in [\widehat {y}_i]_k$ and $\widehat {z}\in [\widehat {y}_{i+1}]_k$ , we have $[\widehat {y}]=[\widehat {y}_i]$ and $[\widehat {y}_{i+1}]=[\widehat {z}]$ in $\widehat {\mathfrak {F}}_0$ (by the definition of $\widehat {E}$ ). Therefore, by Lemma 4.24(2) we have $[\widehat {y}]\mathrel {\widehat {R}_0}[\widehat {y}_{i+1}]$ , and $[\widehat {y}_{i+1}]=[\widehat {z}]$ . This means that we can choose a representative $\widehat {y}$ for each $[\widehat {y}_i]$ such that the cluster $\widehat {E}[\widehat {y}_{i+1}]$ contains a vertical $\Diamond $ -witness $\widehat {z}$ for $\widehat {y}$ . Thus, we may assume that for each i there is $\widehat {z}_{i+1}\in \widehat {X}$ such that $\widehat {y}_{i+1}\mathrel {\widehat {E}}\widehat {z}_{i+1}$ , $\widehat {y}_i\mathrel {\widehat {R}}\widehat {z}_{i+1}$ , and $\widehat {z}_{i+1}$ is added as a vertical $\Diamond $ -witness for $\widehat {y}_i$ with respect to some $\Diamond \psi \in S$ .

Now, $[\widehat {y}_i]\widehat {R}_0[\widehat {y}_j]\implies y_i\mathrel {Q}y_j$ by Lemma 4.19 and Remark 4.23. Let C be the Q-chain

$$\begin{align*}y_1 \mathrel{Q} y_2\dots y_{n-1} \mathrel{Q} y_n \dots\end{align*}$$

in X. Note that for $i\neq j$ since (see Lemma 4.17(1)). Also, since $\widehat {y}_{i+1}\mathrel {\widehat {E}}\widehat {z}_{i+1}$ , we have that $y_{i+1}\mathrel {E}z_{i+1}$ . Since $\widehat {z}_{i+1}$ is a vertical $\Diamond $ -witness for $\widehat {y}_i$ , it must satisfy (V) and Lemma 4.7.

Define a function $f\colon C\to \wp (S)$ by

$$ \begin{align*} f(y_i)=\{\psi\in S \mid y_i\models\psi \}. \end{align*} $$

Let $U\in \wp (S)$ . We claim that $|f^{-1}(U)|\leq 2$ . Suppose $|f^{-1}(U)|\geq 3$ . This implies the existence of distinct $y_i$ , $y_j$ , $y_k$ for which $f(y_i)=f(y_j)=f(y_k)=U$ . By the definition of f, we must have $y_i\mathrel {\sim _S}y_j\mathrel {\sim _S}y_k$ . Without loss of generality, let ${i<j<k}$ . Since $y_{i+1}\mathrel {E}z_{i+1}$ , we have $z_{i+1}\mathrel {Q}y_j$ and $z_{i+1}\mathrel {Q}y_k$ . Also, since $y_i\mathrel {\sim _S}y_j$ , we have $z_{i+1}\mathrel {E}y_j$ by Lemma 4.7(4). Similarly, $z_{i+1}\mathrel {E}y_k$ . Therefore, $y_j\mathrel {E}y_k$ , which is a contradiction to since $j<k$ . Consequently, C must have at most $2\cdot 2^{|S|}$ elements. Thus, the length of $\widehat {C}$ is at most $2^{|S|+1}$ .

Lemma 4.27. If $\widehat {C}$ is a strict $\widehat {R}$ -chain

$$\begin{align*}\widehat{x}_0\mathrel{\widehat{R}}\widehat{x}_1\dots \widehat{x}_{n-1}\mathrel{\widehat{R}}\widehat{x}_n\dots\end{align*}$$

in $\widehat {X}$ such that $\widehat {x}_i\mathrel {\widehat {E}}\widehat {x}_j$ for all i, j, then the length of $\widehat {C}$ is bounded by $2^{|S|}$ .

Proof. The proof is similar to [Reference Bezhanishvili and Khan6, Lemma 7.11], but we have to account for an additional case due to the right commutativity step. First, observe that it is enough to establish the above claim when $\widehat {C}$ is a chain where every relation $\widehat {x}_i\mathrel {\widehat {R}}\widehat {x}_{i+1}$ is introduced at some stage of the construction (otherwise, we can decompose $\widehat {x}_i\mathrel {\widehat {R}}\widehat {x}_{i+1}$ further into a strict chain $\widehat {x}_i\mathrel {\widehat {R}}\widehat {y}_1\dots \widehat {y}_n\mathrel {\widehat {R}}\widehat {x}_{i+1}$ , where the latter relations are indeed introduced through the course of the construction). Now, $\widehat {x}_i\mathrel {\widehat {E}}\widehat {x}_j$ and $\widehat {x}_i\mathrel {\widehat {R}}\widehat {x}_j$ together imply that $\widehat {x}_i\mathrel {E_k}\widehat {x}_j$ and $\widehat {x}_i\mathrel {R_k}\widehat {x}_j$ for some $k<\omega $ . By Lemma 4.17(3), $x_i\mathrel {E}x_j$ and $x_i\mathrel {R}x_j$ . Therefore, we obtain the chain C

$$ \begin{align*} x_0\mathrel{R}x_1\dots x_{n-1}\mathrel{R}x_n\mathrel{R}\dots \end{align*} $$

in the canonical frame of $\mathbf{M}$ .

Claim 4.28. whenever $i\neq j$ .

Proof of the claim.

Fix i and without loss of generality assume that $i<j$ . Define

$$ \begin{align*} U= \bigcap\{v(\alpha)\mid \alpha\in S,\, x_i\models\alpha\} \cap \bigcap \{v(\neg\beta) \mid \beta\in S,\,x_i\not\models\beta\}. \end{align*} $$

We observe that

1. (1) U is a definable subset of X and $x_i\in U$ .

2. (2) For any k, we have $x_i\mathrel {\sim _S}x_k$ iff $x_k\in U$ .

3. (3) We have $\widehat {x}_i\mathrel {R_k}\widehat {x}_{i+1}$ and $\widehat {x}_i\mathrel {E_k}\widehat {x}_{i+1}$ for some $k<\omega $ . By construction, such relations are introduced only in the horizontal $\Diamond $ step (see Remark 4.8). Hence, by (H), there is $\Diamond \delta \in W_{x_i}^\Diamond $ such that $\widehat {x}_{i+1}$ is a $\Diamond $ -witness for $\widehat {x}_i$ with respect to $\Diamond \delta $ . In particular, this implies that $x_i\models \Diamond \delta $ , $x_i\not \models \delta $ , and $x_{i+1}\models \delta $ . This shows that $x_{i+1}\notin U$ , and hence that .

We use the above to show that . Since $\widehat {x}_i$ is introduced in either the initial step, $\exists $ step, $\Diamond $ step, or one of the commutativity steps, we address each separately. In each case, we show that $x_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ for some definable subsets $W_1,W_2$ where $W_2=U$ or $W_2=U\cap V$ with V as in Lemma 4.13.

• • If $\widehat {x}_i$ is introduced in the initial step, then we must have $x_i\in \mathbf {max}\hspace {2pt}v(\neg \varphi )$ . Note that $U\subseteq v(\neg \varphi )$ , and since $x_i\in U$ by (1), we have $x_i\in \mathbf {max}\hspace {2pt}U$ . Furthermore, $U\subseteq E[U]$ , so $x_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ , where $W_1=W_2=U$ .

• • Suppose $\widehat {x}_i$ is introduced in the $\exists $ step. By Lemma 4.6, $x_i\in \mathbf {smax}\hspace {2pt}(E[B]\cap v(\psi ))$ for some definable subset B and $\exists \psi \in S$ . Once again, $U\subseteq v(\psi )$ , and thus $E[B]\cap U\subseteq E[B]\cap v(\psi )$ . This implies that $x_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ , where $W_1=B$ and $W_2=U$ .

• • Suppose $\widehat {x}_i$ is introduced in the $\Diamond $ step. By (H) and (V), $x_i\in \mathbf {max}\hspace {2pt} v(\psi )$ for some $\Diamond \psi \in S$ . Because $U\subseteq v(\psi )$ , and $x_i\in U$ by (1), we have $x_i\in \mathbf {max}\hspace {2pt}U$ . Thus, as in the first case, $x_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ , where $W_1=W_2=U$ .

• • Suppose $\widehat {x}_i$ is introduced in the left commutativity step. The points used to close under left commutativity must be chosen using Lemma 4.11. Therefore, $x_i\in \mathbf {smax}\hspace {2pt}E[B]$ for some definable subset B. Since $x_i \in U$ by (1), we have ${x}_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ , where $W_1=B$ and $W_2=U$ .

• • Finally, suppose $\widehat {x}_i$ is introduced in the right commutativity step. The points used to close under right commutatvity are chosen using Lemma 4.13. Therefore, $x_i\in \mathbf {smax}\hspace {2pt}(E[B]\cap V)$ , where both $B,V$ are definable subsets and V is constructed as in Lemma 4.13. Since $x_i \in U$ by (1), we obtain $x_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ , where $W_1=B$ and $W_2=U\cap V$ .

Now we show that . Suppose otherwise. We first show that $x_j \in W_2$ . This is clear by (2) if $W_2=U$ . Suppose $W_2 = U \cap V$ . Since $x_i\models \Diamond \psi \iff x_j\models \Diamond \psi $ for any $\Diamond \psi \in S$ and $x_i \in W_2 \subseteq V$ , we obtain that $x_j\in V$ (see Lemma 4.13). Thus, $x_j\in U \cap V = W_2$ .

Further, $x_j\mathrel {E}x_i$ and $x_i{\kern-1pt}\in{\kern-1pt} E[W_1]$ imply that $x_j{\kern-1pt}\in{\kern-1pt} E[W_1]$ . Hence, ${x_j{\kern-1pt}\in{\kern-1pt} E[W_1] \cap W_2}$ . However, $j>i+1$ since $x_{i+1}\notin W_2$ (because $x_{i+1}\notin U$ ). Thus, $x_i\mathrel {R}x_{i+1}\mathrel {R}x_j$ , where $x_i\in \mathbf {max}\hspace {2pt}(E[W_1]\cap W_2)$ , $x_{i+1}\notin E[W_1]\cap W_2$ , and $x_j\in E[W_1]\cap W_2$ . This contradicts that $\mathfrak {M}=(\mathfrak {F},v)$ is the canonical model of $\mathbf{M}$ (see Lemma 4.2).

Consequently, the chain C, and thus $\widehat {C}$ , can have at most $2^{|S|}$ points.

Combining Lemmas 4.26 and 4.27, we obtain the following theorem.

Proof. Let

$$ \begin{align*}\widehat{x}_0\mathrel{\widehat{R}}\widehat{x}_1\dots\widehat{x}_{n-1}\mathrel{\widehat{R}}\widehat{x}_n\mathrel{\widehat{R}}\dots\end{align*} $$

be a chain C in $\widehat {\mathfrak {F}}$ , and let C be indexed by $I\subseteq \omega $ . Define $f\colon I\to I$ by

$$ \begin{align*}f(i)=\min\{k\in I\mid \widehat{x}_i\mathrel{\widehat{E}}\widehat{x}_k\}.\end{align*} $$

Let $s_0,s_1,\dots , s_m,\dots $ be an enumeration of $f(I)$ such that $s_i<s_j$ whenever $i<j$ . Consider the corresponding chain

$$ \begin{align*}[\widehat{x}_{s_0}]\mathrel{\widehat{R}_0}[\widehat{x}_{s_1}]\dots [\widehat{x}_{s_{m-1}}]\mathrel{\widehat{R}_0}[\widehat{x}_{s_m}]\dots\end{align*} $$

in $\widehat {\mathfrak {F}}_0$ . By Lemma 4.26, this chain (and hence $f(I)$ ) has size at most $2^{|S|+1}$ . For a fixed m, consider the chain $C\cap [\widehat {x}_{s_m}]$ . By Lemma 4.27, $|C\cap [\widehat {x}_{s_m}]|\leq 2^{|S|}$ . Now observe that

$$ \begin{align*} C=\bigsqcup_{m\in f(I)}(C\cap [\widehat{x}_{s_m}]). \end{align*} $$

Thus, $|C|\leq |f(I)|\cdot 2^{|S|}\leq 2^{2|S|+1}$ , as required.