2.1 Monadic intuitionistic logic

The monadic intuitionistic propositional calculus $\mathsf {MIPC}$ was defined by Prior [Reference Prior38] and it was shown by Bull [Reference Bull11] that $\mathsf {MIPC}$ axiomatizes the monadic fragment of the predicate intuitionistic logic. To define $\mathsf {MIPC}$ , let $\mathcal L$ be the language of propositional intuitionistic logic, and let $\mathcal {L}_{\forall \exists }$ be the enrichment of $\mathcal {L}$ with the quantifier modalities $\forall $ and $\exists $ .Footnote ¹

Algebraic semantics for $\mathsf {MIPC}$ is given by monadic Heyting algebras [Reference Bezhanishvili3, Reference Monteiro and Varsavsky35].

As usual, propositional letters of $\mathcal {L}_{\forall \exists }$ are evaluated as elements of H, the connectives as the corresponding operations of H, and the quantifier modalities as the corresponding modal operators of H. The standard Lindenbaum–Tarski construction then yields:

Kripke semantics for $\mathsf {MIPC}$ is an extension of Kripke semantics for $\mathsf {IPC}$ , and was developed in [Reference Esakia17, Reference Fischer-Servi24, Reference Ono36].

Definition 2.6. An $\mathsf {MIPC}$ -frame is a triple $\mathfrak {F}=(W,R,E)$ where $(W,R)$ is an $\mathsf {IPC}$ -frameFootnote ⁶ and E is an equivalence relation on W satisfying

$$ \begin{align*} (R\circ E)(x)\subseteq (E\circ R)(x) \mbox{ for all } x\in W;\end{align*} $$

that is, if $xEy$ and $yRz$ , then there is $w\in W$ such that $xRw$ and $wEz$ :

We refer to this condition as commutativity. We will sometimes refer to R as a ‘vertical relation’, and to E as a ‘horizontal relation’, as depicted in the diagram above.

Valuations on $\mathsf {MIPC}$ -frames are defined as for $\mathsf {IPC}$ -frames; that is, a valuation $\nu $ on $\mathfrak F=(W,R,E)$ is an assignment of R-upsets of $\mathfrak F$ to propositional letters.Footnote ⁷ As usual, the truth relation in $\mathfrak F$ is defined by induction. The clauses for the connectives $\wedge ,\vee ,\to ,\neg $ are the same as for $\mathsf {IPC}$ -frames:

$$\begin{align*}\begin{array}{lcl} w\vDash_\nu p \quad &\text{iff} & \quad w\in\nu(p); \\ w\vDash_\nu\varphi\wedge\psi \quad &\text{iff}& \quad w\vDash_\nu\varphi \text{ and } w\vDash_\nu\psi;\\ w\vDash_\nu\varphi\vee\psi \quad &\text{iff}& \quad w\vDash_\nu\varphi \text{ or } w\vDash_\nu\psi;\\ w\vDash_\nu\varphi\to\psi \quad &\text{iff}& \quad (\text{for all } v)(wRv \text{ and } v\vDash_\nu\varphi \text{ imply } v\vDash_\nu\psi);\\ w\vDash_\nu\neg\varphi\quad &\text{iff} & \quad (\text{for all } v)(wRv \text{ implies } v\not\vDash_\nu\varphi).\\ \end{array} \end{align*}$$

To extend this to the truth relation for quantifier modalities, we first define a new relation Q on W as the composition $E\circ R$ ; that is, $xQy$ iff there is $z\in W$ such that $xRz$ and $zEy$ :

Then Q is a quasi-order (reflexive and transitive) and $\forall ,\exists $ are interpreted in $\mathfrak F$ as follows:

$$\begin{align*}\begin{array}{lcl} w\vDash_\nu\forall\varphi\quad&\text{iff}&\quad (\text{for all } v)(wQv \text{ implies } v\vDash_\nu\varphi);\\ w\vDash_\nu\exists\varphi\quad&\text{iff}&\quad(\text{there exists } v)(wEv\text{ and } v\vDash_\nu\varphi). \end{array} \end{align*}$$

Sometimes we also write $(\mathfrak F, w) \vDash _\nu \varphi $ to emphasize the underlying frame $\mathfrak F$ or simply $w \vDash \varphi $ in case $\mathfrak F$ and $\nu $ are clear from the context.

There is a close connection between algebraic and relational semantics for $\mathsf {MIPC}$ . To see this, let $\mathfrak F=(W,R,E)$ be an $\mathsf {MIPC}$ -frame. For $x\in W$ , let

$$ \begin{align*} Q(x)=\{y\in W\mid xQy\} \mbox{ and } E(x)=\{y\in W\mid xEy\}. \end{align*} $$

Set $\mathfrak F^+=(\mathsf {Up}(\mathfrak F),\forall ,\exists )$ where $\mathsf {Up}(\mathfrak F)$ is the Heyting algebra of R-upsets of $\mathfrak F$ , and for $U\in \mathsf {Up}(\mathfrak F)$ ,

$$ \begin{align*} \forall U=\{x\in W\mid Q(x)\subseteq U\} \mbox{ and } \exists U=\{x\in W\mid E(x)\cap U\ne\varnothing\}. \end{align*} $$

Then $\mathfrak F^+$ is a monadic Heyting algebra, and every monadic Heyting algebra is represented as a subalgebra of such. To see this, for a monadic Heyting algebra $\mathfrak H=(H,\forall ,\exists )$ , let W be the set of prime filters of H, let R be the inclusion, and let E be defined by $\eta E \zeta $ iff $\eta \cap H_0=\zeta \cap H_0$ , where we recall that $H_0$ is the fixpoint subalgebra of H (see Remark 2.4). Then $\mathfrak H_+ := (W,R,E)$ is an $\mathsf {MIPC}$ -frame (where $\eta Q\zeta $ iff $\eta \cap H_0\subseteq \zeta \cap H_0$ ) and there is an embedding $e:\mathfrak H\to \mathfrak (\mathfrak H_+)^+$ given by

$$ \begin{align*} e(a)=\{\eta\in\mathfrak H_+\mid a\in\eta\}. \end{align*} $$

In general, the embedding e is not onto, so to recognize the e-image of H in the Heyting algebra of upsets, we introduce the concept of a descriptive $\mathsf {MIPC}$ -frame. One way to do this is to introduce topology on an $\mathsf {MIPC}$ -frame.

We recall that a topological space is a Stone space if it is compact Hausdorff and zero-dimensional.Footnote ⁸ A relation R on a Stone space W is continuous if (i) $R(x)$ is closed for each $x\in W$ and (ii) U clopen implies $R^{-1}(U)$ is clopen, where

$$ \begin{align*} R^{-1}(U)=\{x\in W\mid xRu \mbox{ for some } u\in U\}. \end{align*} $$

As follows from Esakia’s representation of Heyting algebras [Reference Esakia13], for a Heyting algebra H, there is a Stone topology on the set W of prime filters of H generated by the basis

$$ \begin{align*} \{e(a)\setminus e(b)\mid a,b\in H\}, \end{align*} $$

the inclusion relation R on W is continuous, and e is a Heyting isomorphism from H onto the Heyting algebra of clopen R-upsets of W.

By [Reference Bezhanishvili4, Theorem 13], if $\mathfrak H=(H,\forall ,\exists )$ is a monadic Heyting algebra, then $(W,R,E)$ is a descriptive $\mathsf {MIPC}$ -frame, which we denote by $\mathfrak H_*$ , and e is an isomorphism from $\mathfrak H$ onto the monadic Heyting algebra $(\mathfrak H_*)^*$ of clopen R-upsets of $\mathfrak H_*$ . Thus, every monadic Heyting algebra can be thought of as the algebra of clopen R-upsets of some descriptive $\mathsf {MIPC}$ -frame. This representation together with Theorem 2.5 yields:

If the descriptive $\mathsf {MIPC}$ -frame is finite, then the topology is discrete, and hence finite descriptive $\mathsf {MIPC}$ -frames are simply finite $\mathsf {MIPC}$ -frames. It is well known that $\mathsf {MIPC}$ has the finite model property (FMP):

This was first proved by Bull [Reference Bull10] using algebraic semantics. Bull’s proof contained a gap, which was later filled by Fischer-Servi [Reference Fischer-Servi23] and Ono [Reference Ono36] independently of each other. For a more frame-theoretic proof, using the technique of selective filtration, see [Reference Gabbay, Kurucz, Wolter and Zakharyaschev25, Section 10.3].

We finish Section 2.1 by recalling an important property of descriptive $\mathsf {MIPC}$ -frames, which will be useful later on.

The next lemma states that every point in the E-saturation of clopen A sees a point that is maximal in the E-saturation of A. The proof follows from the result of Fine [Reference Fine21] and Esakia [Reference Esakia16, Reference Esakia20] that can be phrased as follows: If A is a closed subset of a descriptive $\mathsf {IPC}$ -frame, then for each $x\in A$ there is $y\in \max A$ such that $xRy$ . Since A clopen implies that $E(A)$ is closed (see Remark 2.8), the proof is a consequence of the Fine-Esakia lemma.

2.2 Monadic modal logics

Let $\mathcal {ML}$ be the basic propositional modal language (with one modality $\Box $ ). As usual, the least normal modal logic will be denoted by $\mathsf {K}$ , and normal modal logics are normal extensions of $\mathsf {K}$ .

Let $\mathcal {ML_{\forall }}$ be the bimodal language which enriches $\mathcal {ML}$ with the modality $\forall $ . We use the abbreviation $\exists \varphi $ for $\neg \forall \neg \varphi $ .

Algebraic semantics for monadic modal logics is given by monadic modal algebras.

Kripke semantics for mm-logics is given by the augmented Kripke frames of Esakia [Reference Esakia17].

Definition 2.17. An augmented Kripke frame is a triple $\mathfrak {F}=(W,R,E)$ where $(W,R)$ is a Kripke frameFootnote ¹³ and E is an equivalence relation on W satisfying commutativity, i.e., $(R\circ E)(x)\subseteq (E\circ R)(x)$ for all $x\in W$ ; that is, if $xEy$ and $yRz$ , then there is $w\in W$ such that $xRw$ and $wEz$ :

As with $\mathsf {MIPC}$ -frames, we may refer to R as a ‘vertical relation’, and to E as a ‘horizontal relation’, as depicted in the diagram above.

Valuations on augmented Kripke frames are defined analogously to Kripke frames; that is, a valuation $\nu $ on an augmented Kripke frame $\mathfrak {F}=(W,R,E)$ assigns subsets of W to propositional letters. The truth relation clauses for the connectives $\vee , \neg $ , the modality $ \Box $ , and its dual $\Diamond $ are defined as for Kripke frames:

$$ \begin{align*} &x \vDash_{\nu} p \quad &\text{ iff }&\quad x\in\nu(p); \\ &x \vDash_{\nu}\psi\vee\chi \quad &\text{ iff } & \quad x \vDash_{\nu}\psi\text{ or } x \vDash_{\nu}\chi; \\ &x \vDash_{\nu}\neg\psi \quad& \text{ iff } & \quad x \not\vDash_{\nu}\psi; \\ & x \vDash_{\nu}\square\psi \quad & \text{ iff }&\quad (\text{for all } y\in W) (xRy\Rightarrow y\vDash_{\nu}\psi); \\ &x \vDash_{\nu}\lozenge\psi \quad & \text{ iff }&\quad (\text{there exists } y\in W )(xRy\text{ and } y \vDash_{\nu}\psi).\\ &&&\hspace{-100pt}\text{The modality }\forall \text{ and its dual }\exists\text{ are interpreted via the relation }E\text{ as follows:}\\ & x\vDash_{\nu}\forall\varphi\quad &\text{iff} &\quad (\text{for all } y\in W)(xEy\Rightarrow y\vDash_{\nu}\varphi);\\ & x\vDash_{\nu}\exists\varphi\quad & \text{iff} &\quad(\text{there exists } y\in W)(xEy\text{ and }y\vDash_{\nu}\varphi). \end{align*} $$

We also use the notation $(\mathfrak F, w) \vDash _\nu \varphi $ or $w \vDash \varphi $ .

As in the case of $\mathsf {MIPC}$ , there is a close connection between algebraic and relational semantics for mm-logics. For an augmented Kripke frame $\mathfrak F=(W,R,E)$ , set $\mathfrak F^+=(\wp (\mathfrak F),\square ,\forall )$ where $\wp (\mathfrak F)$ is the powerset of $\mathfrak F$ , and for $U\in \mathsf {Up}(\mathfrak F)$ ,

$$ \begin{align*} \square U=\{x\in W\mid R(x)\subseteq U\} \mbox{ and } \forall U=\{x\in W\mid E(x)\subseteq U\}. \end{align*} $$

Then $\mathfrak F^+$ is an mm-algebra, and every mm-algebra is represented as a subalgebra of such. To see this, for an mm-algebra $\mathfrak B=(B,\square ,\forall )$ , let W be the set of ultrafilters of B, and let R and E be defined by

$$ \begin{align*} \eta R \zeta \mbox{ iff }\square a\in\eta \mbox{ implies } a\in\zeta, \mbox{ and } \eta E \zeta \mbox{ iff } \eta\cap B_0=\zeta\cap B_0. \end{align*} $$

Then $\mathfrak B_+=(W,R,E)$ is an augmented Kripke frame and there is an embedding $e:\mathfrak B\to \mathfrak (\mathfrak B_+)^+$ given by

$$ \begin{align*} e(a)=\{\eta\in\mathfrak B_+\mid a\in\eta\}. \end{align*} $$

In general, the embedding e is not onto, so to recognize the e-image of $\mathfrak B$ in the powerset, we introduce the concept of a descriptive augmented Kripke frame. As in the case of $\mathsf {MIPC}$ , we do this by introducing topology on augmented Kripke frames.

As follows from the representation of modal algebras, for a modal algebra B, there is a Stone topology on the set W of ultrafilters of B generated by the basis $\{e(a)\mid a\in B\}$ , the relation R on W is continuous, and e is a modal isomorphism from B onto the modal algebra of clopen subsets of W.

If $\mathfrak B=(B,\square ,\forall )$ is an mm-algebra, then $(W,R,E)$ is a descriptive augmented Kripke frame, which we denote by $\mathfrak B_*$ , and e is an isomorphism from $\mathfrak B$ onto the mm-algebra $(\mathfrak B_*)^*$ of clopen subsets of $\mathfrak B_*$ . Thus, every mm-algebra can be thought of as the algebra of clopen subsets of some descriptive augmented Kripke frame.

2.3 $\mathsf {MS4}$ , $\mathsf {MGrz}$ , and $\mathsf {MGL}$

We next focus on the least monadic extension $\mathsf {MS4}$ of the modal logic $\mathsf {S4}$ .

As in the case of $\mathsf {MIPC}$ , we have the following standard completeness results:

We also have that $\mathsf {MS4}$ has the finite model property (see [Reference Bezhanishvili and Carai6] and the references therein).

Let $\mathfrak {F}=(W,R,E)$ be a descriptive $\mathsf {MS4}$ -frame and $A \subseteq W$ . The R-maximal points of A and the R-maximum of A are defined as in Definition 2.11. In the context of $\mathsf {MS4}$ -frames, we also need the notion of quasi-R-maximal points.

Note that $\max A\subseteq \text {q}\hspace {-.25em}\max A$ as R is reflexive, but not conversely. The following lemma is a consequence of the Fine-Esakia lemma [Reference Esakia16, Reference Esakia20, Reference Fine21] for descriptive $\mathsf {S4}$ -frames.

Again, we have the following standard completeness results:

It is well known that an $\mathsf {S4}$ -frame $\mathfrak {F}=(W,R)$ is a $\mathsf {Grz}$ -frame iff R is a Noetherian partial order; that is, a partial order with no infinite ascending chains (of distinct points). Thus, if $\mathfrak {F}$ is finite, then $\mathfrak {F}$ is a $\mathsf {Grz}$ -frame iff R is a partial order.

It is a result of Esakia that a descriptive $\mathsf {S4}$ -frame $\mathfrak {F}=(W,R)$ is a descriptive $\mathsf {Grz}$ -frame iff for each clopen $A \subseteq W$ the R-maximal and quasi-R-maximal points of A coincide. These results clearly hold for $\mathsf {MGrz}$ as well.

As before, we have the following standard completeness results:

It is well known that a Kripke frame $\mathfrak {F}=(W,R)$ is a $\mathsf {GL}$ -frame iff R is transitive and dually well founded (no infinite ascending chains). Call R a strict partial order if R is irreflexive and transitive. If W is finite, then $\mathfrak {F}$ is a $\mathsf {GL}$ -frame iff R is a strict partial order.

A characterization of descriptive $\mathsf {GL}$ -frames was originally established by Esakia and given in [Reference Abashidze1]. It generalizes directly to descriptive $\mathsf {MGL}$ -frames. For a transitive frame $\mathfrak {F}=(W,R)$ and $A\subseteq W$ , define the irreflexive maximum of A by

$$ \begin{align*} \qquad\mu(A)=\{x\in A \mid R(x)\cap A=\varnothing\}. \end{align*} $$

Thus, a descriptive augmented Kripke frame is a descriptive $\mathsf {MGL}$ -frame iff it is transitive and each point in a clopen set is either in the irreflexive maximum of the clopen or sees a point in the irreflexive maximum. It was observed by Japaridze that $\mathsf {MGL}$ has the finite model property.

3.1 Gödel translation

The Gödel translation extends to the monadic setting by defining

$$ \begin{align*} (\forall\varphi)^t & = \square\forall \varphi^t,\\ (\exists\varphi)^t & = \exists \varphi^t. \end{align*} $$

Using algebraic semantics, Fisher-Servi [Reference Fischer-Servi22, Reference Fischer-Servi23] proved that this provides a full and faithful embedding of $\mathsf {MIPC}$ into $\mathsf {MS4}$ . The proof also yields a full and faithful embedding of $\mathsf {MIPC}$ into $\mathsf {MGrz}$ . Below we give an alternate proof of this result, using relational semantics. The proof extends a semantical proof that $\mathsf {IPC}\vdash \varphi $ iff $\mathsf {S4}\vdash \varphi ^t$ as given, e.g., in [Reference Chagrov and Zakharyaschev12, pp. 96–97].

For notational simplicity, we abbreviate the formula $\square \forall \psi $ as $\blacksquare \psi $ and the formula $\lozenge \exists \psi $ as $\blacklozenge \psi $ . Observe that this keeps the duality between box and diamond since $\blacksquare \psi =\square \forall \psi =\neg \lozenge \neg \neg \exists \neg \psi ,$ which is provably equivalent to $\neg \lozenge \exists \neg \psi =\neg \blacklozenge \neg \psi $ .

Remark 3.1. The modalities $\blacksquare ,\blacklozenge $ are $\mathsf {S4}$ -modalities which can be modeled using the relation $Q=E\circ R$ , i.e., we have

$$\begin{align*}& w \vDash\blacksquare\varphi\quad\text{iff}\quad (\text{for all } v)(wQv \text{ implies } v\vDash\varphi);\\ & w \vDash\blacklozenge\varphi\quad\text{iff}\quad (\text{there exists } v)(wQv\text{ and } v\vDash\varphi). \end{align*}$$

Using this notation, the $\forall $ -step in the Gödel translation is

$$ \begin{align*} (\forall\varphi)^t & = \blacksquare \varphi^t. \end{align*} $$

For an $\mathsf {MS4}$ -frame $\mathfrak {F}=(W, R, E)$ define an equivalence relation $\sim $ on $\mathfrak {F}$ by

$$ \begin{align*} x\sim y\text{ iff } xRy \text{ and } yRx. \end{align*} $$

Let $[x]$ be the equivalence class of x, and let $W_{\sim }=W/{\sim }$ be the set of all equivalence classes. Define $R_{\sim }$ and $E_{\sim }$ on $W_{\sim }$ by

$$ \begin{align*} [x] R_{\sim} [y] \quad &\text{iff} \quad xRy; \quad \\ [x] E_{\sim} [y] \quad &\text{iff} \quad xQy \text{ and } yQx. \end{align*} $$

That $E_\sim $ is well defined follows from $R \circ Q \circ R \subseteq Q$ which is true by commutativity in $\mathfrak F$ and transitivity of R. Let $\mathfrak {F}_{\sim }=(W_{\sim }, R_{\sim }, E_{\sim })$ . Set $Q_\sim = E_\sim \circ R_\sim $ .

Given a valuation $\nu $ on $\mathfrak F$ , define a valuation $\nu _{\sim }$ on $\mathfrak F_{\sim }$ by

$$ \begin{align*} \nu_{\sim}(p)=\{[x]\mid x\in \nu(\square p)\}. \end{align*} $$

Clearly $\nu _{\sim }(p)$ is an upset. We call $\mathfrak F_{\sim }$ the skeleton of $\mathfrak F$ and $(\mathfrak F_{\sim }, \nu _\sim )$ the skeleton of $(\mathfrak F, \nu )$ .

Conversely, given an $\mathsf {MIPC}$ -frame $\mathfrak F$ , we regard it as an $\mathsf {MS4}$ -frame. In addition, if $\mathfrak F$ is finite, then we regard it as a finite $\mathsf {MGrz}$ -frame. If $\nu $ is a valuation on the $\mathsf {MIPC}$ -frame $\mathfrak F$ , then we regard it as a valuation on the $\mathsf {MGrz}$ -frame $\mathfrak F$ .

The following lemma describes how the above frame transformations behave with respect to the Gödel translation. It is proved by induction on the complexity of $\varphi $ .

Proof. If $\mathfrak F$ is an $\mathsf {MIPC}$ -frame, then $\mathfrak F_\sim $ is isomorphic to $\mathfrak F$ . Therefore, (1) follows from (2). To prove (2), by [Reference Chagrov and Zakharyaschev12, Lemma 3.81], it is sufficient to only consider the case for the modalities $\forall $ and $\exists $ . Let $\varphi =\forall \psi $ . Then

$$\begin{align*} \quad[x] \vDash \forall\psi \quad &\Leftrightarrow\quad (\mbox{for all } [y]) ([x]Q_\sim [y] \Rightarrow [y]\vDash \psi) \\ &\Leftrightarrow\quad (\mbox{for all } [y]) ([x]Q_\sim[y] \Rightarrow y\vDash \psi^t) \quad\text{(Inductive Hypothesis)} &\\ &\Leftrightarrow\quad (\mbox{for all } y) (xQy \Rightarrow y \vDash \psi^t) \quad\text{(Lemma 3.2(2))} \\ &\Leftrightarrow\quad x\vDash \blacksquare \psi^t \\ &\Leftrightarrow\quad x\vDash (\forall\psi)^t. \end{align*}$$

Next let $\varphi =\exists \psi $ . If $x \models (\exists \psi )^t $ , then there is y with $x Ey $ and $y \models \psi ^t $ . Therefore, $[y] \models \psi $ by the inductive hypothesis, and $[x] E_{\sim} [y]$ by Lemma 3.2(1). Thus, $[x] \models \exists \psi $ . Conversely, suppose that $[x] \models \exists \psi $ . Then there is $[y]$ with $[x] E_\sim [y]$ and $[y] \models \psi $ . Therefore, $y Q x$ by the definition of $E_\sim $ . Thus, there is $x'$ with $y R x'$ and $x' E x$ . By the definition of $R_\sim $ , we have $[y] R_\sim [x']$ . So $[x'] \models \psi $ by persistence in $\mathfrak F_\sim $ . Consequently, $x' \models \psi ^t$ by the inductive hypothesis, so $x\models\exists\psi^t$ , and hence $x\models (\exists\psi)^t$ .⊣

3.2 Splitting translation

Next we discuss the splitting translation in the monadic setting. The key here is Esakia’s observation that the splitting translation does not yield a faithful embedding of $\mathsf {MGrz}$ into $\mathsf {MGL}$ . Since this result is unpublished, we give a proof of it.

Descriptive $\mathsf {MGL}$ -frames have the property that clusters in the irreflexive maximum of an E-saturated clopen are clean.

Proof. Suppose there exist clopen A and $m\in \mu (E(A))$ with $E(m)$ dirty. Then there are $x,y\in E(m)$ with $xRy$ , $xEy$ , and $x\not =y$ . By commutativity, there is $w$ such that $mRw$ and $wEy$ , as shown below:

Since $y\in E(A)$ we have $w\in E(A)$ . But this contradicts $R(m)\cap E(A)=\varnothing $ . Thus, we cannot have a dirty cluster in $\mu (E(A))$ .⊣

As a consequence of Lemma 3.7, we obtain:

We next show that the splitting translation of the Gödel translation of the monadic version of Casari’s formula

$$ \begin{align*} \mathsf{MCas: }\quad\forall\left(\left(p\rightarrow\forall p\right)\rightarrow\forall p\right)\rightarrow \forall p \end{align*} $$

is provable in $\mathsf {MGL}$ .

Since $\square \forall p\leftrightarrow \square \forall \square p$ is provable in $\mathsf {MS4}$ , it is straightforward to check that $(\mathsf {MCas})^t$ is provably equivalent to $\square \forall \big (\square (\square p\rightarrow \square \forall p)\rightarrow \square \forall p\big )\rightarrow \square \forall p$ . Using the notation $\blacksquare $ introduced above, we have that $(\mathsf {MCas})^t$ is:

$$ \begin{align*} \mathsf{M_\Box Cas}: \quad\blacksquare\big(\square(\square p\rightarrow\blacksquare p)\rightarrow\blacksquare p\big)\rightarrow\blacksquare p. \end{align*} $$

We use $\blacksquare ^{+}\psi $ to abbreviate $\forall \psi \wedge \square \forall \psi =\square ^{+}\forall \psi $ . Then the splitting translation of $\mathsf {M_\Box Cas}$ is

$$ \begin{align*} (\mathsf{M_\Box Cas})^s = \blacksquare^{+}\big(\square^{+}(\square^{+}p\rightarrow\blacksquare^{+} p)\rightarrow\blacksquare^{+} p\big)\rightarrow\blacksquare^{+} p. \end{align*} $$

Proof. Suppose $\mathfrak {F}=(W,R,E)$ is a descriptive $\mathsf {MGL}$ -frame. We will prove that $\mathfrak {F}\vDash (\mathsf {M_\Box Cas})^s$ . Let $\nu $ be a valuation on $\mathfrak F$ , $x \in \mathfrak F$ , and $x\not \vDash _\nu \blacksquare ^{+}p$ . We show that $x\not \vDash \blacksquare ^{+}(\square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+}p)\rightarrow \blacksquare ^{+}p)$ . Let $A=W\setminus \nu (\blacksquare ^{+}p)$ . Then $x \in A$ and so by Lemma 2.29, $x\in \mu (A)\cup R^{-1}\mu (A)$ . If $x \in R^{-1}\mu (A)$ , then there is $x' \in \mu (A)$ with $x R x'$ . If $x \in \mu (A)$ , we let $x' = x$ . From $x' \in \mu (A)$ it follows that $x' \in A$ , so $x' \not \models \blacksquare ^{+}p= \forall p \wedge \Box \forall p$ . We show that $x' \not \models \forall p$ . If $x' \not \models \Box \forall p$ , then there is y with $x'Ry$ and $y \not \models \forall p$ . Therefore, $y \not \models \blacksquare ^{+} p$ , so $y \in A$ . But this contradicts $x' \in \mu (A)$ . Thus, $x' \not \models \forall p$ . So there is w with $w E x'$ and $w \not \models p$ . We show that

$$ \begin{align*} w \not \models \square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+} p) \rightarrow \blacksquare ^{+} p. \end{align*} $$

Since $w\not \vDash p$ , we have $w\not \vDash p\wedge \square p$ , so $w\not \vDash \square ^{+} p$ , and hence $w\vDash \square ^{+}p\rightarrow \blacksquare ^{+}p$ . Let $w R z$ . By commutativity, there is y such that $x'Ry$ and $yEz$ . Since $x' \in \mu (A)$ , we have $y \not \in A$ . Therefore, $y\vDash \blacksquare ^{+}p$ , so $y\vDash \forall p$ , and hence $z\vDash \forall p$ :

In fact, if $zRt$ , then $wRt$ by transitivity, and so by the same reasoning as above we have $t\vDash \forall p$ . It follows that $z\vDash \Box \forall p$ , and so $z\vDash \blacksquare ^{+}p$ . Thus, $z\vDash \square ^{+}p\rightarrow \blacksquare ^{+}p$ , and hence $w\vDash \square (\square ^{+}p\rightarrow \blacksquare ^{+}p)$ . This together with $w\vDash \square ^{+}p\rightarrow \blacksquare ^{+}p$ yields $w\vDash \square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+} p)$ . Since $w\not \vDash \blacksquare ^{+} p$ , we obtain $w \not \vDash \square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+} p) \rightarrow \blacksquare ^{+} p$ .

If $x = x'$ , then $x E w$ , and so $x \not \vDash \forall (\square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+} p) \rightarrow \blacksquare ^{+} p)$ . Otherwise, $x R x'$ and $x' Ew$ imply $x Q w$ , so $x \not \models \blacksquare (\square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+} p) \rightarrow \blacksquare ^{+} p)$ . Thus, in either case, $x \not \models \blacksquare ^+ (\square ^{+}(\square ^{+}p\rightarrow \blacksquare ^{+} p) \rightarrow \blacksquare ^{+} p)$ as desired. This yields $x\vDash (\mathsf {M_\Box Cas})^s$ . Since x was arbitrary, $\mathfrak {F}\vDash (\mathsf {M_\Box Cas})^s$ . Because $\mathfrak F$ is an arbitrary descriptive $\mathsf {MGL}$ -frame, by Theorem 2.28(2), $\mathsf {MGL}\vdash (\mathsf {M_\Box Cas})^s$ .⊣

Proof. Consider the $\mathsf {MGrz}$ -frame $\mathfrak {F}=(W,R,E)$ where $W=\{x,y\}$ , $R=\{(x,x),(y,y),(x,y)\}$ , and $E=W^{2}=\{(x,x),(y,y),(x,y),(y,x)\}$ , as shown below:

The arrow represents the nontrivial R-relation and the circle represents that both points are in the same E-equivalence class. It is easy to see that this is an $\mathsf {MGrz}$ -frame. Let $\nu $ be a valuation on $\mathfrak {F}$ with $\nu (p)=\{y\}$ . We first show that

$$ \begin{align*} x\vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p). \end{align*} $$

Note that $x\not \vDash \blacksquare p$ and $y\not \vDash \blacksquare p$ , but since $y\vDash p$ and y only sees itself (with respect to R), we have $y\vDash \square p$ . Therefore, $y\not \vDash \square p\rightarrow \blacksquare p$ , so $x\not \vDash \square (\square p\rightarrow \blacksquare p)$ , and hence $x\vDash \square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p$ . Moreover, since $y\not \vDash \square (\square p\rightarrow \blacksquare p)$ , we have $y\vDash \square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p$ , and hence $x\vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p)$ . However, $x\not \vDash \blacksquare p$ as $xQx$ and $x\not \vDash p$ . Thus, $x\not \vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p)\rightarrow \blacksquare p$ , so $\mathfrak {F}\not \vDash _{\mathsf {MGrz}}\mathsf {M_\Box Cas}$ , and hence $\mathsf {MGrz}\not \vdash \mathsf {M_\Box Cas}$ .⊣

As an immediate consequence of Theorems 3.9 and 3.10, we obtain:

4.1 $\mathsf {M^{+}IPC}$

Definition 4.1. The logic $\mathsf {M^{+}IPC}$ is defined as the extension of $\mathsf {MIPC}$ by $\mathsf {MCas}$ :

$$ \begin{align*} \mathsf{M^{+}IPC}=\mathsf{MIPC}+\mathsf{MCas}. \end{align*} $$

Recall from Definition 3.6 that a cluster of an $\mathsf {MIPC}$ -frame is called clean if no distinct points in the cluster are R-related. The following semantic characterization of $\mathsf {M^+IPC}$ -frames was established by Esakia. For a proof see [Reference Bezhanishvili5, Lemma 38]. It states that a descriptive $\mathsf {MIPC}$ -frame is a descriptive $\mathsf {M^+IPC}$ -frame iff the cluster of each point in the R-maximum of the E-saturation of a clopen set is clean.

As a consequence of Lemma 4.2, we obtain:

4.2 $\mathsf {M^{+}Grz}$

Definition 4.5. The logic $\mathsf {M^{+}Grz}$ is the extension of $\mathsf {MGrz}$ by $\mathsf {M_\Box Cas}$ :

$$ \begin{align*} \mathsf{M^{+}Grz}=\mathsf{MGrz}+\mathsf{M_\Box Cas}. \end{align*} $$

In order to obtain a semantic characterization of $\mathsf {M^+Grz}$ , which is an analogue of Lemma 4.2, we require the following lemma.

We now have the necessary machinery to prove a semantic characterization of $\mathsf {M^+Grz}$ , which states that a descriptive $\mathsf {MGrz}$ -frame is a descriptive $\mathsf {M^+Grz}$ -frame iff the cluster of every point in the maximum of the E-saturation of a clopen set is clean.

Proof. First suppose $\mathfrak {F}\not \vDash \mathsf {M_\Box Cas}$ . Then there is $x\in W$ such that

$$ \begin{align*} x\not \vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p)\rightarrow \blacksquare p, \end{align*} $$

and hence $x\vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p)$ but $x\not \vDash \blacksquare p$ . Since $x\not \vDash \blacksquare p$ , there is $x' \in W$ such that $xQx'$ and $x'\not \vDash p$ . Let $A=\{w\in W \mid w\not \vDash p\}$ . Then $x'\in A$ , and as $x'Ex'$ , we have $x' \in E(A)$ . Because A is clopen, so is $E(A)$ . By Lemma 2.26(2), there is $y \in \max E(A)$ with $x'R y$ . If $E(y)$ is dirty, then we are done. So assume that $E(y)$ is clean. We show that this leads to a contradiction. Since $y \in E(A)$ , there is $y' \in A$ with $y E y'$ . By Lemma 4.7(1), $y' \in \max E(A)$ . As $x Q y'$ and $x\vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p)$ , we have $y'\vDash \square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p$ . Because $y' \in A$ , we have $y'\not \vDash p$ and since $y'Qy'$ , we have $y'\not \vDash \blacksquare p$ , so we must have $y'\not \vDash \square (\square p\rightarrow \blacksquare p)$ . Thus, there is $z\in W$ such that $y'Rz$ and $z\not \vDash \square p\rightarrow \blacksquare p$ , which means $z\vDash \square p$ but $z\not \vDash \blacksquare p$ . Because $z\not \vDash \blacksquare p$ , there exist $w',w\in W$ such that $zRw'Ew$ and $w\not \vDash p$ (see the diagram below):

Now, since $w\not \vDash p$ , we have $w\in A$ and hence $w'\in E(A)$ . Thus, $y'Rw'$ and $w'\in E(A)$ , so by R-maximality of $y'$ in $E(A)$ , we must have $y'=w'$ . But then $y'R z$ and $z R y'$ , and so by Lemma 4.7(2), $y'=z$ . This, however, is a contradiction since $z\vDash \square p$ , hence $z\vDash p$ , whereas $y'\not \vDash p$ .

For the converse, suppose that A is clopen and $m\in \max E(A)$ with $E(m)$ dirty. First observe that since m is maximal in $E(A)$ , from $m Q t$ it follows that $t \in E(m)$ for all $t \in E(A)$ . Indeed, if $m Q t$ for $t \in E(A)$ , then there is $t'$ with $m R t'$ and $t' E t$ . Since $t' \in E(A)$ , we have $t' =m$ by maximality of m in $E(A)$ . Thus, $t \in E(m)$ .

Now, since $E(m)$ is dirty, there are $x , x' \in E(m)$ with $x R x'$ and $x \neq x'$ . In particular, $x \not \in \max E(A)$ . Since $E(A)$ is clopen, $\max E(A)$ is closed (see, e.g., [Reference Esakia20, Section III.2]). Thus, we can find clopen B such that $x\in B$ but $B\cap \max E(A)=\varnothing $ , as shown below:

Choose a valuation $\nu $ with $\nu (p)=W\setminus (B\cap E(A))$ . Note that $\nu $ is well-defined as B and $E(A)$ are clopen. We aim to show that $x\vDash \blacksquare (\square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p)$ but $x\not \vDash \blacksquare p$ . Since $x \in B\cap E(A)$ , we have $x \not \models p$ . This implies that $x \not \models \blacksquare p$ because $x Q x$ . To finish the argument it suffices to show that $y \models \square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p$ for all y with $x Q y$ . So let $x Q y$ and assume that $y\not \models \blacksquare p$ . Then there is z with $yQ z$ and $z \not \models p$ . Therefore, $z \in B\cap E(A)$ and there is $z'$ with $y R z'$ and $z' E z$ . Clearly $z' \in E(A)$ . By Lemma 2.26(2), there is $t \in \max E(A)$ with $z'R t$ :

Since $t \in \max E(A)$ , we have $t \not \in B$ , so $t \models p$ and if $t R v$ for $t \neq v$ , then $v \not \in E(A)$ by maximality of t, so $v \models p$ . Thus, $t \models \Box p$ . On the other hand, $x Q y$ , $y R z' $ , and $z' R t$ imply $m Q t$ . As we saw above, this means $t \in E(m)$ , and so $t Ex$ . Since $x \not \models p$ , we have $t \not \models \blacksquare p$ . This yields that $t \not \models \square p\rightarrow \blacksquare p$ , so $y \not \models \square ( \square p\rightarrow \blacksquare p )$ , and hence $y \models \square (\square p\rightarrow \blacksquare p)\rightarrow \blacksquare p$ as desired.⊣

As a consequence of Lemma 4.8, we obtain:

4.3 The translations $\mathsf {M^{+}IPC}\to \mathsf {M^{+}Grz}\to \mathsf {MGL}$

The remaining part of the paper establishes the finite model property for the logics $\mathsf {M^+IPC}$ and $\mathsf {M^+Grz}$ . We finish this section by explaining how a proof of Esakia’s claim is then obtained.

Let R be a binary relation. We recall that the irreflexive reduction of R, denoted $R^{i}$ , is defined by

$$ \begin{align*} aR^{i}b \text{ iff } aRb \text{ and } a\not=b; \end{align*} $$

and the reflexive closure of R, denoted $R^{r}$ , is defined by

$$ \begin{align*} aR^{r}b \text{ iff } aRb \text{ or } a=b. \end{align*} $$

For an augmented Kripke frame $\mathfrak {F}=( W,R, E)$ , let $\mathfrak {F}^i=( W,R^i, E)$ and $\mathfrak {F}^{r}=( W,R^{r}, E)$ . Following the terminology of [Reference Chagrov and Zakharyaschev12, pp. 98–99], we call $\mathfrak {F}^i$ the irreflexive reduction and $\mathfrak {F}^{r}$ the reflexive closure of $\mathfrak {F}$ .

We are ready to provide a proof of Esakia’s claim.

This concludes lifting the original correspondences given by Goldblatt, Boolos, and Kuznetsov and Muravitsky from the propositional setting to the monadic setting, verifying Esakia’s claim. Combining this with Japaridze’s result of arithmetical completeness for $\mathsf {MGL}$ yields provability interpretations of $\mathsf {M^{+}IPC}$ and $\mathsf {M^{+}Grz}$ .

5.1 The construction

We start with a formula $\varphi $ , a descriptive $\mathsf {M^+IPC}$ -frame $\mathfrak F=(W, R, E)$ , and a valuation $\nu $ on $\mathfrak F$ such that $\mathfrak F \not \models \varphi $ . By modifying the construction in [Reference Gabbay, Kurucz, Wolter and Zakharyaschev25, Section 10.3], we will construct a sequence of finite $\mathsf {M^{+}IPC}$ -frames $\mathfrak {F}_{h}=(W_{h},R_{h},E_{h})$ such that $\mathfrak {F}_{h}\subseteq \mathfrak {F}_{h+1}$ for all $h<\omega $ . For each point $t\in W_{h}$ that we select, we will be creating a copy of some original point in W. We give each added point a new name, say t, and let $\widehat {t}$ denote the original point in W that t was copied from and will behave similar to. Thus, it is possible to have two different points $x_{1}$ and $x_{2}$ in our new frame, where $\widehat {x_{1}}=\widehat {x_{2}}$ . The main difference between our construction and the construction given in [Reference Gabbay, Kurucz, Wolter and Zakharyaschev25, Section 10.3] will be seen in the $\rightarrow $ -step, which requires a more careful selection of new points.

To start the construction, let $\mathfrak {F}_{0}=(W_{0},R_{0},E_{0})$ where

$$ \begin{align*} W_{0}=\{t_{0}\},\quad R_{0}=W_{0}^{2}, \quad E_{0}=W_{0}^{2}, \end{align*} $$

and $\widehat {t_{0}}$ is a point in W such that $\widehat {t_0}$ is from a clean cluster and is maximal with respect to $\varphi $ . The existence of such $\widehat {t_0}$ follows from Lemma 5.2(4). Moreover, let $W^{\forall H}_{-1}= \varnothing $ .

Let $\mathsf {Sub}(\varphi )$ be the set of subformulas of $\varphi $ , and let $(W', R', E')$ be any of our frames in the construction. To each $t \in W'$ we associate the following subsets of $\mathsf {Sub}(\varphi )$ :

$$\begin{align*} \Sigma^{\exists}(t) &= \{\exists\delta\in \mathsf{Sub}(\varphi) \mid \widehat{t}\ \vDash\exists\delta\text\},\\ \Sigma^{\forall H}(t) &=\{\forall\beta\in \mathsf{Sub}(\varphi) \mid \widehat{t}\text{ is maximal wrt }\forall\beta\},\\ \Sigma^{\forall V}(t) &= \{\forall\gamma\in \mathsf{Sub}(\varphi) \mid \widehat {t}\ \not\vDash\forall\gamma\text{ but is not maximal wrt }\forall\gamma\},\\ \Sigma^{\rightarrow}(t) &= \{\alpha\rightarrow\sigma\in \mathsf{Sub}(\varphi) \mid \widehat {t}\ \not\vDash\alpha\rightarrow\sigma \text{ and }\widehat{t}\not\vDash\alpha\}. \end{align*}$$

These are precisely the subformulas of $\varphi $ whose truth-value at $\widehat {t}$ is relevant for constructing our countermodel. Note that if $\alpha\rightarrow\sigma\in\Sigma^\rightarrow(t)$ , then $\widehat{t}$ is not maximal with respect to $\alpha\rightarrow\sigma$ .

Suppose $\mathfrak {F}_{h-1}=(W_{h-1},R_{h-1},E_{h-1})$ has already been constructed so that $\mathfrak {F}_{h-1}$ is a finite $\mathsf {M^+IPC}$ -frame and $E(\,\widehat {w}\;)$ is a clean cluster for each $w\in W_{h-1}$ . We construct $\mathfrak {F}_{h}$ by applying the four steps described below. They are designed to add the necessary witnesses required by the formulas in the sets $\Sigma ^{\exists }(t)$ , $\Sigma ^{\forall H}(t)$ , $\Sigma ^{\forall V}(t)$ , and $\Sigma ^{\rightarrow }(t)$ , respectively. In the $\exists $ -step we ensure that for each formula in $\Sigma ^{\exists }(t)$ the point t has an E-successor that witnesses the existential statement. In the $\forall H$ -step we ensure that for each formula in $\Sigma ^{\forall H}(t)$ the point t has an E-successor that witnesses the refutation of the universal statement. In the vertical steps $\forall V$ and $\rightarrow $ we make sure that t has the necessary R-successors that are maximal with respect to the formulas in $\Sigma ^{\forall V}(t)$ and $\Sigma ^{\rightarrow }(t)$ , respectively. In each step of the construction we add also points to witness commutativity. Note that the first three of the following four steps are only done once per cluster. This is enough since all points of a cluster in $\mathfrak F$ agree on refuting an $\forall $ - or $\exists $ -formula and points from a clean cluster agree whether such a refutation is maximal.

Roughly speaking, points are added to the construction in the following order: In the first round the cluster of the starting point $t_{0}$ is built by adding points for formulas in $\Sigma ^{\exists }(t_0)$ and $\Sigma ^{\forall H}(t_0)$ . After this, no more points are added to this cluster. We call this the ‘bottom cluster’ of our frame. The first round of the construction proceeds by adding vertical witnesses for each formula in $\Sigma ^{\forall V}(t_0)$ and closing each such cluster by adding points for commutativity. The first round then finishes by adding for each point t in the ‘bottom cluster’ vertical witnesses for the formulas in $\Sigma ^{\rightarrow }(t)$ and closing under commutativity. In the next round all these newly built clusters will possibly be enlarged in the horizontal steps and then new vertical witnesses will be added in the $\forall V$ - and $\rightarrow $ -steps.

$\exists $ -step $($ Horizontal $)$ : Let $W^\exists _{h} = W_{h-1}$ , $R^\exists _{h} = R_{h-1}$ , and $E^\exists _{h} = E_{h-1}$ . For each $E^{\exists }_{h}(t)\subseteq W^{\exists }_{h}\backslash W_{h-1}^{\forall H}$ , if $\exists \delta \in \Sigma ^{\exists }(t)$ but there is no $s\in W^\exists _{h}$ already such that $tE^{\exists }_{h}s$ and $\widehat {s}\ \vDash \delta $ , then we add a point s to $W^\exists _{h}$ with $\widehat {s} \models \delta $ and $\widehat {t} E \widehat {s}$ . Such a point $\widehat {s}$ exists in W since $\widehat {t} \models \exists \delta $ . We then add the ordered pairs $(s,s)$ to $R^\exists _{h}$ , the ordered pairs $(t,s)$ to $E^\exists _{h}$ , and generate the least equivalence relation.

$\forall H$ -step $($ Horizontal $)$ : Let $W^{\forall H}_{h} = W^\exists _{h}$ , $R^{\forall H}_{h} = R^\exists _{h}$ , and $E^{\forall H}_{h} = E^\exists _{h} $ . For each $E^{\forall H}_{h}(t)\subseteq W^{\forall H}_{h}\backslash W_{h-1}^{\forall H}$ , if $\forall \beta \in \Sigma ^{\forall H}(t)$ but there is no $s\in W_{h}^{\forall H}$ already such that $tE_{h}^{\forall H}s$ and $\widehat {s}\ \not \vDash \beta $ , then we add a point s to $W_{h}^{\forall H}$ with $\widehat {s}\ \not \models \beta $ and $\widehat {t} E \widehat {s}$ . Such a point $\widehat {s}$ exists in W since $\widehat {t}$ is maximal with respect to $\forall \beta $ . We then add the ordered pairs $(s,s)$ to $R^{\forall H}_{h}$ , the ordered pairs $(t,s)$ to $E^{\forall H}_{h}$ , and generate the least equivalence relation. $\forall $ V-step $($ Vertical $)$ : Let $W^{\forall V}_{h} = W^{\forall H}_{h} $ , $R^{\forall V}_{h} = R^{\forall H}_{h}$ , and $E^{\forall V}_{h} = E^{\forall H}_{h}$ . For each $E^{\forall V}_{h}(t)\subseteq W^{\forall V}_{h}\backslash W_{h-1}^{\forall H}$ , consider $\forall \gamma \in \Sigma ^{\forall V}(t)$ . Since $\widehat {t}\ \not \vDash \forall \gamma $ , we can pick a point $\widehat {s} \in W$ as in Lemma 5.2(2). We add the point s to $W_{h}^{\forall V}$ and $(t,s)$ to $R_{h}^{\forall V}$ .

Since W satisfies commutativity, for each $w\in E_{h}^{\forall V}(t)$ , there is $z_{w}\in W$ such that $\widehat {w}Rz_{w}$ and $z_{w}E \widehat {s}$ . To ensure commutativity is satisfied in our new frame, we add the points $s_{w}$ to $W_{h}^{\forall V}$ where $\widehat {s_{w}}=z_{w}$ . We then add $(w,s_{w})$ to $R_{h}^{\forall V}$ and take the reflexive and transitive closure. We also add $(s_{w},s)$ to $E_{h}^{\forall V}$ and generate the least equivalence relation.

$\rightarrow $ -step $($ Vertical $)$ : Let $W^{\rightarrow }_{h} = W^{\forall V}_{h} $ , $R^{\rightarrow }_{h} = R^{\forall V}_{h}$ , and $E^{\rightarrow }_{h} = E^{\forall V}_{h}$ . For each $t\in W_{h}^{\forall H} \backslash W_{h-1}^{\forall H}$ (hence including any points added in the horizontal steps above, but not in the previous vertical step), consider all $\alpha \rightarrow \sigma \in \Sigma ^{\rightarrow }(t)$ such that there is no $s\in W^{\rightarrow }_{h}$ already such that $tR^{\rightarrow }_{h}s$ , $\widehat{s}\vDash\alpha$ , and $\widehat{s}\not\vDash\sigma$ . Consider

$$ \begin{align*} A=[W \setminus \nu(\alpha\rightarrow\sigma)]\cap\bigcap_{\psi\in\mathsf{Sub}(\varphi)}\{\nu(\psi):\widehat{t}\ \vDash\psi\}. \end{align*} $$

Then A is clopen and $\widehat {t} \in A$ , so by Lemma 5.2(3) there is $z \in A$ with $z \in \max E(A)$ , $\widehat {t} Q z$ , and $E(z)$ clean. We add the point s to $W_{h}^{ \rightarrow }$ where $\widehat {s}=z$ (s is a distinct new copy of z) and $(t,s)$ to $R_{h}^{ \rightarrow }$ .