Proof. That the original axiom follows from (1) is obvious since $\exists $ is increasing. For the same reason, the axiom implies the $(\geq )$ direction in (1), while the $(\leq )$ direction follows since $\exists $ is idempotent. By taking Boolean negation, we see that (2) is equivalent to (1). That the axiom is equivalent to (3) is known, but not immediate; see [Reference Bezhanishvili and Carai3, Lemma 2.5]. Taking Boolean negation yields that (3) is equivalent to the inequality $\lozenge \forall \leq \forall \lozenge $ , which in turn is equivalent to (4) in the same manner that (1) is equivalent to the original axiom.

Proof. First suppose that $xQy$ and $a\in x\cap H_\blacksquare $ . Then there is z such that $xRz$ and $zEy$ . Therefore, $x\cap H_\square \subseteq z$ and $z\cap B_0 =y\cap B_0$ . Since $a\in H_\blacksquare $ , we have $a=\Box \forall a=\forall \Box \forall a$ (where the last equality follows from Lemma 2.4(2)), so $a\in H_\square \cap B_0$ . But then from $a\in x$ it follows that $a\in z$ , which then implies that $a\in y$ . Thus, $x\cap H_\blacksquare \subseteq y$ .

Conversely, suppose that $x\cap H_\blacksquare \subseteq y$ . Let F be the filter generated by $(x\cap H_\square )\cup (y\cap B_0)$ and I the ideal generated by $B_0\setminus y$ . We show that $F \cap I = \varnothing $ . Otherwise there are $a\in x\cap H_\square $ , $b\in y\cap B_0$ , and $c\in B_0\setminus y$ such that $a\wedge b \le c$ . Therefore, $a\le b\to c$ , so $a \le \Box (b \to c)$ because $a\in H_\square $ . Since $b,c\in B_0$ , we have $\Box (b\to c)\in H_\blacksquare $ . Thus, $\Box (b\to c)\in x\cap H_\blacksquare \subseteq y$ , and so $b\to c\in y$ . Consequently, $c \in y$ because $b \in y$ . The obtained contradiction proves that $F\cap I=\varnothing $ . Therefore, there is an ultrafilter z such that $x\cap H_\square \subseteq z$ and $z\cap B_0=y\cap B_0$ . But then $xRz$ and $zEy$ , yielding that $xQy$ .

Proof. The modal filters and $\blacksquare $ -filters are literally the same lattice. Therefore, so are the closed Q-upsets and the closed E-saturated R-upsets of $\mathfrak {F}$ . This gives the equivalence of (1), (2) and (5), (6). Note that the $\blacksquare $ -fixpoints of $\mathfrak {A}$ are exactly the $\square $ -fixpoints of $\mathfrak {A}_0$ , which yields the equivalence of (2) and (3), and also (4) by [Reference Esakia, Bezhanishvili and Holliday13, Theorem 2.4.17]. Finally, these are equivalent to (5) by [Reference Esakia, Bezhanishvili and Holliday13, Theorem 3.4.16].

Proof. (1) It is well known (see, e.g., [Reference Burris and Sankappanavar10, Section II.8]) that $\mathfrak {A}$ is s.i. iff $\mathfrak {A}$ has a least nontrivial congruence. By the above theorem, this is equivalent to $\mathfrak {F}$ having the largest closed Q-upset Y different from X. The complement of Y is the nonempty open set of Q-roots of $\mathfrak {F}$ .

(2) $\mathfrak {A}$ is simple iff the only nontrivial congruence is $A^2$ [Reference Burris and Sankappanavar10, Section II.8]. Thus, using (1), $\mathfrak {A}$ is simple iff $Y=\varnothing $ , which is equivalent to $\mathfrak {F}$ being a Q-cluster.

Proof. Let $\mathbf {V}$ be a semisimple subvariety of $\mathbf {MS4}$ and let $\mathfrak {A} \in \mathbf {V}$ be s.i. Then $\mathfrak {A}$ is simple, so the dual $\textsf {MS4}$ -frame $\mathfrak {F}$ of $\mathfrak {A}$ is a Q-cluster by Theorem 3.5(2). Therefore, Q is an equivalence relation on $\mathfrak {F}$ , and hence $\mathfrak {A}\models \blacklozenge \blacksquare p \to \blacksquare p$ . Thus, $\mathfrak {A}\in \mathbf {MS4_S}$ , and so $\mathbf {V}\subseteq \mathbf {MS4_S}$ .

Proof. Since $\mathfrak {A}$ is an $\mathsf {MS4_S}$ -algebra, $\blacklozenge $ is an $\mathsf {S5}$ -operator. Moreover,

$$\begin{align*}\exists \blacklozenge a = \exists \Diamond \exists a = \Diamond \exists a = \blacklozenge a = \blacklozenge \exists a \end{align*}$$

(the second equality follows from Lemma 2.4(1)). Therefore, $(B, \blacklozenge , \exists )$ is an $\mathsf {S5}^2$ -algebra that in addition satisfies $\exists \blacklozenge a = \blacklozenge a$ for each $a\in B$ . Thus, $(B, \blacklozenge , \exists )$ belongs to a proper subvariety of $\mathbf {S5}^2$ , which is locally finite by [Reference Bezhanishvili6, Section 4]. Consequently, $(B, \blacklozenge , \exists )$ is locally finite.

Proof. As we already pointed out, $\mathfrak {A}_S$ is finite by Lemma 3.11. Moreover, $\lozenge '$ is an $\mathbf {S4}$ -operator on $\mathfrak {A}_S$ (see [Reference McKinsey and Tarski27, Lemma 2.3]). For the reader’s convenience, we sketch the proof of this result.

• • That $\lozenge ' 0 = 0$ is clear since $0 \in B' \cap K$ .

• • That $\lozenge '(a \vee b) = \lozenge ' a \vee \lozenge ' b$ follows from distributivity since the meets involved in the definition of $\lozenge '$ are finite.

• • That $a \leq \lozenge 'a$ follows from the definition of $\lozenge ' a$ .

• • To see that $\lozenge ' \lozenge ' a \leq \lozenge ' a$ , it is enough to observe that if $b\in B'\cap K$ , then $a\le b$ iff $\Diamond ' a\le b$ .

We next show that $\exists \lozenge ' a \leq \lozenge ' \exists a$ , or equivalently that $\exists \lozenge ' \exists a = \lozenge ' \exists a$ , i.e. that $\lozenge ' \exists a$ is a $\exists $ -fixpoint for each $a\in \mathfrak {A}_S$ . First observe that if $b \in B' \cap K$ with $\exists a \leq b$ , then $\forall b \in B' \cap K$ (since $\lozenge \forall \lozenge = \forall \lozenge $ ) and $\exists a \leq \forall b$ . Because $\forall b \leq b$ , we have $\lozenge ' \exists a = \bigwedge \left \{\forall b : b \in B' \cap K, \exists a \leq b\right \}$ . But this is a finite meet of $\exists $ -fixpoints and hence an $\exists $ -fixpoint.

Finally, we check $\blacklozenge ' \blacksquare ' a \leq \blacksquare ' a$ for each $a\in B'$ , where $\blacklozenge ' = \lozenge ' \exists $ and $\blacksquare ' = {-} \blacklozenge ' {-}$ . Since $\lozenge \exists a \in B'$ (because $B'$ is closed under $\blacklozenge $ ), $\lozenge ' \exists a = \lozenge \exists a$ , so $\blacklozenge ' = \blacklozenge \vert _{B'}$ , and hence the inequality holds because $\mathfrak {A}$ is an $\mathsf {MS4_S}$ -algebra.

Proof. If $\mathsf {MS4_S}\not \vdash \varphi $ , then there is an $\mathsf {MS4_S}$ -algebra $\mathfrak {A} = (B, \lozenge , \exists )$ and an n-tuple $\overline {a}$ such that $\varphi (\overline {a}) \neq 1$ in $\mathfrak {A}$ . Let S be the set of subterms of $\varphi (\overline {a})$ . Since S is finite, $\mathfrak {A}_S = (B', \lozenge ', \exists )$ is a finite $\mathsf {MS4_S}$ -algebra by the previous lemma. Moreover, the definition of $\lozenge '$ ensures that if $\lozenge a \in B'$ , then $\lozenge ' a = \lozenge a$ . Therefore, the computation of $\varphi (\overline {a})$ in $\mathfrak {A}_S$ is identical to that in $\mathfrak {A}$ , and hence $\varphi (\overline {a}) \neq 1$ in $\mathfrak {A}_S$ . Thus, $\varphi $ is falsified in $\mathfrak {A}_S$ .

Proof. (1) If $\mathsf {MS4_S} \not \vdash \varphi $ , then by the previous theorem, $\varphi $ is falsified on a finite $\mathsf {MS4_S}$ -algebra $\mathfrak {A}$ . Let n be the depth of $\mathfrak {A}$ . Then $\mathfrak {A}\models \mathsf {MS4_S}[n]$ , so $\mathsf {MS4_S}[n] \not \vdash \varphi $ , and hence $\bigcap _n \mathsf {MS4_S}[n]\not \vdash \varphi $ .

(2) This is obvious since $\mathsf {MS4_S}$ is finitely axiomatizable and has the fmp.

Proof. First suppose that $\mathbf {V}$ is locally finite. Then for every n, the free n-generated $\mathbf {V}$ -algebra is finite. Letting $f(n)$ be its cardinality, $f:\omega \to \omega $ is our desired function, and hence (2) is satisfied. Moreover, (1) is satisfied since the $\mathbf {S4}$ -reduct of $\mathbf {V}$ is a uniformly locally finite class (that is, there is a uniform finite bound on the size of an n-generated subalgebra of an algebra from this class), and so it generates a locally finite variety (see [Reference Mal’cev, Smirnov and Taĭclin26, p. 285]). Thus, $\mathbf {V}$ is of finite depth by the Segerberg–Maksimova theorem.

Conversely, suppose that $\mathbf {V}$ satisfies (1) and (2). By [Reference Bezhanishvili5, Theorem 3.7(4)], it suffices to give a finite bound on the cardinality of every n-generated s.i. $\mathfrak {A} \in \mathbf {V}$ . By (2), $\mathfrak {A}_0$ is an $f(n)$ -generated $\mathsf {S4}$ -algebra, and it is of finite depth because $\mathfrak {A}$ is of finite depth by (1). Thus, ${\lvert {B_0} \rvert } \leq k(n)$ by the Segerberg–Maksimova theorem. Since $B_0$ is the $\exists $ -fixpoints of $\mathfrak {A}$ , we have that $\mathfrak {A}$ is $(n + k(n))$ -generated as an $\mathsf {S4}$ -algebra, and thus we have some $m(n)$ such that ${\lvert {B} \rvert } \leq m(n + k(n))$ .

Proof. The formula $\mathsf {alt}_k^0$ is obtained from the well-known formula

$$\begin{align*}\mathsf{alt}_k = \square p_1 \vee \square(p_1 \to p_2) \vee \ldots \vee \square(p_1 \wedge p_2 \wedge \ldots \wedge p_k \to p_{k+1}) \end{align*}$$

by substituting $\forall p_i$ for $p_i$ . Let $\mathfrak {F} = (X, R, E)$ be the dual of $\mathfrak {A}$ . Since $\mathfrak {A}$ is s.i., $\mathfrak {F}$ is strongly Q-rooted by Theorem 3.5(1). Because the universe of the subalgebra $\mathfrak {A}_0$ is exactly $\forall $ -fixpoints of $\mathfrak {A}$ , $\mathfrak {A} \models \mathsf {alt}_k^0$ iff $\mathfrak {A}_0 \models \mathsf {alt}_k$ . By Remark 2.10, the dual space of $\mathfrak {A}_0$ is $\mathfrak {F}_0 = (X/E, \overline {R})$ , which is a rooted descriptive $\mathsf {S4}$ -frame. Since $\mathsf {alt}_k$ is a canonical formula ([Reference Blackburn, de Rijke and Venema9, Definition 4.30] together with [Reference Chagrov and Zakharyaschev11, Theorem 5.16]), $\mathsf {alt}_k$ is valid on $\mathfrak {F}_0$ iff it is valid on the underlying Kripke frame of $\mathfrak {F}_0$ ([Reference Blackburn, de Rijke and Venema9, Proposition 5.85]). It is well known [Reference Chagrov and Zakharyaschev11, Proposition 3.45] that $\mathsf {alt}_k$ holds in a Kripke frame iff the number of alternatives of each point is $\leq k$ or, in the rooted transitive case, the number of points in the frame is $\leq k$ . Thus, $\mathsf {alt}_k^0$ holds on $\mathfrak {A}$ iff ${\lvert {X/E} \rvert } \leq k$ or, equivalently, ${\lvert {\mathfrak {A}_0} \rvert } \leq 2^k$ .

Proof. We show that in this case Theorem 4.2(2) is always satisfied and the criterion reduces to being of finite depth. Let $\mathfrak {A} \in \mathbf {V}$ be s.i. and n-generated. By the above lemma, ${\lvert {\mathfrak {A}_0} \rvert } \leq 2^k$ . Thus, $\mathfrak {A}_0$ is (at most) $2^k$ -generated.

Proof. Suppose $\mathfrak {F}^*$ is generated by $\bar {g}$ , and let K be a non-trivial correct partition. Then K corresponds to a proper subalgebra of $\mathfrak {F}^*$ that couldn’t contain all of the $g_i$ . That is, there is some $g_i$ that is not K-saturated. So there are $x \in g_i$ and $y \not \in g_i$ that are K-related. Thus, $xKy$ but $c(x) \neq c(y)$ , and we’ve shown that any non-trivial correct partition K cannot satisfy $K \subseteq C$ .

Now suppose $\mathfrak {F}^*$ is not generated by $\bar {g}$ . Then $\bar {g}$ generates a proper subalgebra $\mathfrak {A}$ , which gives rise to a non-trivial correct partition K, defined by

$$\begin{align*}x K y \text{ iff for all }a \in \mathfrak {A} \; (x \in a \leftrightarrow y \in a).\end{align*}$$

Now, if $c(x) \neq c(y)$ , then $x \in g_i$ and $y \in\ -g_i$ for some $g_i \in \mathfrak {A}$ , so $\neg (xKy)$ . Thus, $K \subseteq C$ .

Proof. By [Reference Magill24, Theorem 2.1], X is compact Hausdorff. We show that X is zero-dimensional. For this it suffices to separate distinct points of X by a clopen subset of X (see, e.g., [Reference Johnstone19, p. 69]). First suppose that $x, y \in X_0$ . Since $X_0$ is zero-dimensional, there is a clopen set $U\subseteq X_0$ containing x and missing y. Because $X_0$ is locally compact, x has a compact neighborhood K in $X_0$ . Therefore, there is a clopen set V with $x\in V \subseteq U\cap K$ . But then V is a compact clopen of $X_0$ , and hence a clopen subset of X separating x and y. The points $k_1$ and $k_2$ are separated by $g_1 \cup \left \{k_1\right \}$ which is clopen of X by definition. Finally, $x \in X_0$ and $k_i$ are separated by any compact clopen neighborhood K of x in $X_0$ , which is a clopen set of X.

Proof. Since X is a Stone space by the above lemma, it remains to show that $E_1, E_2$ are continuous. We show that $E_1$ is continuous. The proof for $E_2$ is symmetric. Observe that all finite-index rows (i.e., $[0, \omega ] \times \left \{j\right \}$ for $j < \omega $ ) are evidently clopen, while the “top row” $\left \{(i, \omega ) : i < \omega \right \} \cup \left \{k_1,k_2\right \}$ is closed but not open (its complement is the union of all finite-index rows). Hence, $E_1$ is point-closed.

It is left to show that U clopen implies $E_1(U)$ is clopen. By [Reference Esakia, Bezhanishvili and Holliday13, Theorem 3.1.2(IV)], it is enough to verify the following two conditions:

1. (1) If $y \not \in E_1(x)$ , then there is a partition into two $E_1$ -saturated open sets separating x and y.

2. (2) For all x and open V, if $E_1(x) \cap V \neq \varnothing $ , then there is an open neighborhood U of x with $E_1(y) \cap V \neq \varnothing $ for all $y \in U$ .

For (1), since $y \not \in E_1(x)$ , x and y are in distinct rows. Therefore, one of them must be in a row of finite index, say $R_n = [0,\omega ] \times \{ n \}$ with $n < \omega $ (if both are in rows of finite index, take n to be the least index). Then $[0, \omega]$ and its complement provide a partition of X into two $E_1$ -saturated open sets separating x and y.

For (2), we consider cases: If $x = (i, j)$ for $i, j < \omega $ , $\left \{x\right \}$ is an appropriate neighborhood. If $x = (\omega , j)$ for $j < \omega $ , then $[0,\omega ] \times \left \{j\right \}$ is an appropriate neighborhood. Suppose $x = (i, \omega )$ for $i<\omega $ . If $E_1(x) \cap V$ contains $(i', \omega )$ for $i'<\omega $ , then V contains a neighborhood $\left \{i'\right \} \times [n, \omega ]$ for $n < \omega $ , so $\left \{i\right \} \times [n, \omega ]$ is an appropriate neighborhood of x. If $E_1(x) \cap V$ contains $k_1$ , then V contains some $V' \cup \left \{k_1\right \}$ with $g_1 - V'$ compact in $X_0$ , as sets of this form are the only basic open neighborhoods of $k_1$ . Then there must be some n with $(g_1- V')\cap [n, \omega ]^2 = \varnothing $ (indeed any $U \subseteq X_0$ compact has this property since otherwise $\left \{X_0-[n, \omega ]^2 : n < \omega \right \}$ would be an open cover of U without a finite subcover). Therefore, $g_1 \cap [n, \omega ]^2 \subseteq V' \subseteq V$ , and again $\left \{i\right \} \times [n, \omega ]$ is an appropriate neighborhood of x. If $E_1(x) \cap V$ contains $k_2$ , then by the same argument we have an n with $g_2 \cap [n, \omega ]^2 \subseteq V$ and the same neighborhood works. Finally, suppose $x = k_s$ for $s \in \left \{1,2\right \}$ . If $E_1(x) \cap V$ contains $(i, \omega )$ for $i < \omega $ , then V contains $\left \{i\right \} \times [n, \omega ]$ for some n, and $(g_s \cap [n, \omega ]^2) \cup \left \{k_s\right \}$ is an appropriate basic open neighborhood of x. If $E_1(x) \cap V$ contains $k_t$ for $t \neq s$ , then by the same argument as before we have $g_t \cap [n, \omega ]^2 \subseteq V$ for some n, and the same neighborhood $(g_s \cap [n, \omega]^2) \cup \{k_s\}$ works.

Proof. Let $g = g_1 \cup \left \{k_1\right \}$ (see Figure 3). We claim $\mathfrak {F}^* = \langle g \rangle $ . Suppose not. By the coloring theorem, there exists a non-trivial correct partition K of X such that every class of K is contained in g or ${-}g$ . Since it is non-trivial, K must identify two points in distinct rows or columns (by assumption we cannot have $k_1 K k_2$ ). By Remark 5.6, this is to say that two distinct rows or columns must be $\overline {K}$ -related. Let $C_i = \left \{i\right \} \times [0, \omega ]$ be the i-th column and $R_j = [0, \omega ] \times \left \{j\right \}$ the j-th row. Observe that $C_0$ cannot be related to $C_i$ for $i> 0$ since otherwise a point in ${-}g \cap C_i$ would be K-related to a point in ${-}g \cap C_0 = \varnothing $ .

Now suppose $C_{i_1}$ and $C_{i_2}$ are $\overline {K}$ -related for $0 < i_1 < i_2 \leq \omega $ . Then there must be some $j_2 \in [i_1, i_2)$ so that $(i_2, j_2) K (i_1, j_1)$ for some $j_1 \in [0, i_1)$ (since all points in ${-}g \cap C_{i_2}$ must be K-related to points in ${-}g \cap C_{i_1}$ ). Therefore, rows $j_1$ and $j_2$ are $\overline {K}$ -related, with $0 \leq j_1 < j_2 < i_2$ . Thus, $(j_2, j_2) K (i_0, j_1)$ for some $i_0 \in [0, j_1]$ . We now conclude that columns $i_0$ and $j_2$ are $\overline {K}$ -related, and note that $0 \leq i_0 < i_1$ , $0 < j_2 < i_2$ , and $i_0 < j_2$ . So from our assumption of two $\overline {K}$ -related columns, we have found two $\overline {K}$ -related columns of strictly lower index, and iterating this process will eventually reveal that column $0$ must be $\overline {K}$ -related to some non-zero column, which is a contradiction by the previous paragraph.

Finally, suppose $R_{j_1}$ and $R_{j_2}$ are $\overline {K}$ -related for $0 \leq j_1 < j_2 \leq \omega $ . Then $(j_2, j_2) K (i, j_1)$ (or $k_1 K (i, j_1)$ in the case $j_2 = \omega $ ) for some $i \in [0, j_1]$ . But then columns i and $j_2$ are $\overline {K}$ -related, with $i < j_2$ , which is a contradiction by the last paragraph.

Consequently, such a K cannot exist, and we conclude that $\mathfrak {F}^*$ is generated by g. There is an evident homomorphism $f : \mathfrak {F}^* \to \mathcal {P}(\omega \times \omega )$ given by $U \mapsto U \cap (\omega \times \omega )$ . Then $f(g) = \left \{(i, j) : i \leq j\right \}$ , and f is an isomorphism onto its image (because $\omega \times \omega $ is dense in X). Thus, $\mathfrak{F}^*$ is isomorphic to the subalgebra of $\mathcal{P}(\omega \times \omega)$ generated by $f(g)$ , which is exactly the Erdös–Tarski algebra.

Question 5.14. Let $(X, R, E)$ be a finitely generated descriptive $\mathsf {MS4}$ -frame. Is $D_1 = \max X$ or any $D_n$ a clopen (admissible, definable) set?

Question 5.15. Does there exist a finitely generated descriptive $\mathsf {MS4}$ -frame whose finite layers consist only of limit points?

Construction 6.8. Let $\mathfrak {F} = (X, E_1, E_2)$ be a descriptive $\mathsf {S5}_2$ -frame. We let $\mathcal {L} = X / E_2$ be the quotient space and $\pi _{\mathcal {L}} : X \to \mathcal {L}$ the quotient map. We set $T(\mathfrak {F}) = (X \cup \mathcal {L}, R, E)$ , where

• • $X \cup \mathcal {L}$ is the (disjoint) union of X and $\mathcal {L}$ ,

• • E is the smallest equivalence on $X \cup \mathcal {L}$ containing $E_2$ along with

  $$\begin{align*}\left\{(x, \alpha) : x \in X, \alpha \in \mathcal{L}, x \in \alpha\right\}, \end{align*}$$

• • $R = E_1 \cup (X \times \mathcal {L}) \cup (\mathcal {L} \times \mathcal {L})$ .

In the case that $\lvert\mathfrak{F}\rvert$ is finite, it follows that $\lvert T(\mathfrak{F}) \rvert \leq 2\lvert \mathfrak{F} \rvert$ and $\lvert T(\mathfrak{F})^* \rvert \leq \lvert \mathfrak{F}^* \rvert^2.$

Proof. Suppose $U \subseteq X$ is clopen. Then $\pi _{\mathcal {L}}^{-1}(\pi _{\mathcal {L}}[U]) = E_2(U)$ , which is clopen by continuity of $E_2$ . Since $\pi _{\mathcal {L}}$ is a quotient map, $\pi _{\mathcal {L}}[U]$ is clopen.

Proof. Note that $E_2$ is a separated partition of X (but in general not correct with respect to $E_1$ in the sense of Definition 5.5) since any $(x, y) \not \in E_2$ can be separated by a $E_2$ -saturated clopen (this is a property of any continuous quasi-order; see [Reference Esakia, Bezhanishvili and Holliday13, Theorem 3.1.2]). This ensures $\mathcal {L}$ is a Stone space [Reference Koppelberg, Monk and Bonnet22, Lemma 8.4]. Thus, so is $X \cup \mathcal {L}$ (the union is disjoint).

Clopen sets in $T(\mathfrak {F})$ are of the form $U \cup V$ , with U clopen in X and V clopen in $\mathcal {L}$ . We have

• • $E(x) = E_2(x) \cup \left \{E_2(x)\right \}$ for $x \in X$ ;

• • $E(\alpha ) = \alpha \cup \left \{\alpha \right \}$ for $\alpha \in \mathcal {L}$ ;

• • $E(U \cup V) = E_2(U) \cup \pi _{\mathcal {L}}[U] \cup V \cup \pi _{\mathcal {L}}^{-1}(V)$ .

The first two items show that E-clusters are closed. In the third item, every set on the right hand side is clopen, by continuity of $E_2$ and the fact that $\pi _{\mathcal {L}}$ is a clopen map (Lemma 6.9). Thus, E is continuous. For R, we have

• • $R(x) = E_1(x) \cup \mathcal {L}$ for $x \in X$ ;

• • $R(\alpha ) = \mathcal {L}$ for $\alpha \in \mathcal {L}$ ;

• • $ R^{-1}(U \cup V) = \begin {cases} E_1(U) & V = \varnothing , \\ X \cup \mathcal {L} & \text {otherwise}. \end {cases} $

By the first two items, R is point-closed, which together with the third yields that R is continuous.

Now observe that $Q = ER$ is the total relation on $T(\mathfrak {F})$ (i.e., $Q = (X \cup \mathcal {L})^2$ ) because for each $x\in X$ we have $\mathcal {L}\subseteq R(x)$ , so $X \cup \mathcal {L} = ER(x)$ . Therefore, every point of $T(\mathfrak {F})$ is a Q-root and, in particular, $RE \subseteq ER$ . Finally, $T(\mathfrak {F})$ is of R-depth 2 by construction. Thus, $T(\mathfrak {F})$ is a Q-rooted descriptive $\mathsf {MS4_S}[2]$ -frame.

Proof. This follows from the explicit description of $R^{-1}$ and E on clopen sets in Lemma 6.10. Also, the relative complementation and modal operators are definable using the clopen set $D_2 \in T(\mathfrak {F})^*$ , e.g., by using precisely the definitions from the preceding paragraph.

Proof. (1) We first show $\widehat {K}$ is separated. If $x, y \in D_2$ and $\neg (x \widehat {K} y)$ , then $\neg (x K y)$ and they can be separated by a K-saturated clopen subset of $D_2$ , which is also $\widehat {K}$ -saturated (since $\widehat {K}$ relates no points in different layers). Any $x \in D_2$ and $\alpha \in D_1$ can be separated by $D_2$ which is $\widehat {K}$ -saturated by the same reason. Now suppose $\alpha , \beta \in D_1$ and $\neg (\alpha \widehat {K} \beta )$ . Then $\neg (x K y)$ for any $x \in \alpha , y \in \beta $ , and so any such $x, y$ can be separated by a K-saturated clopen $A\subseteq D_2$ . By Lemma 6.9, $\pi _{\mathcal {L}}[A]$ is a clopen subset of $D_1$ separating $\alpha $ and $\beta $ . To see it is $\widehat {K}$ -saturated, let $\gamma \in \pi _{\mathcal {L}}[A]$ and $\gamma \widehat {K} \delta $ . Then there is $x \in A \cap \gamma $ and $y \in \delta $ with $x K y$ (x may be chosen from A by the remarks at the end of Definition 5.5). Since A is K-saturated, $y \in A \cap \delta $ , and hence $\delta \in \pi _{\mathcal {L}}[A]$ .

We now show $\widehat {K}$ is correct with respect to R. Suppose $x, y \in D_2$ . If $x \widehat {K} y R z$ for $z \in D_2$ , then $x K y E_1 z$ , so $x E_1 y' K z$ by correctness of K, and hence $x R y' \widehat {K} z$ . If $x \widehat {K} y R \alpha $ for $\alpha \in D_1$ , then $x R \alpha \widehat {K} \alpha $ (by definition of R). Suppose $\alpha , \beta \in D_1$ . If $\alpha \widehat {K} \beta R \gamma $ for $\gamma \in D_1$ (the only possibility), then $\alpha R \gamma \widehat {K} \gamma $ (again by definition of R). In any case, $R\widehat {K} \subseteq \widehat {K} R$ .

Finally, we show $\widehat {K}$ is correct with respect to E. Suppose $x, y \in D_2$ . If $x \widehat {K} y E z$ for $z \in D_2$ , then $x K y E_2 z$ , so $x E_2 y' K z$ , and hence $x E y' \widehat {K} z$ . If $x \widehat {K} y E \alpha $ for $\alpha \in D_1$ , then $\alpha = E_2(y)$ , and $E_2(x) \, \overline {K} \, E_2(y)$ . So $x \; E \; E_2(x) \; \widehat {K} \; \alpha $ . Suppose $\alpha , \beta \in D_1$ . If $\alpha \widehat {K} \beta E z$ for $z \in D_2$ (the only non-trivial possibility), then $\beta = E_2(z)$ . So we must have $z K x$ for some $x \in \alpha $ , and hence $\alpha E x \widehat {K} z$ . In any case, $E\widehat {K} \subseteq \widehat {K} E$ . We conclude that $\widehat {K}$ is a correct partition of $T(\mathfrak {F})$ .

(2) We exhibit an isomorphism $f : T(\mathfrak {F}/K) \to T(\mathfrak {F})/\widehat {K}$ . Let $f(K(x)) = K(x)$ on K-classes (i.e., the identity on the common second layer of both frames) and $f(\overline {E_2} (K(x))) = \overline {K} (E_2(x))$ on the additional points. To check continuity, it suffices to check on clopen subsets of the top layer only (since $\widehat {K}$ identifies no points across layers and f is the identity on the bottom layers); such a clopen can be identified with a $\overline {K}$ -saturated clopen U of $\mathfrak {F}$ , and we have

$$ \begin{align*} f^{-1}(U) =& \left\{\overline{E_2}(K(x)) : E_2(x) \in U\right\} \text{ is clopen in } T(\mathfrak{F}/K) \\ \text{iff } & \left\{K(x) : E_2(x) \in U\right\} \text{ is clopen in } \mathfrak{F}/K \\ \text{iff } & \left\{x : E_2(x) \in U\right\} \text{ is clopen in } \mathfrak{F}. \end{align*} $$

The last set is precisely $\pi _{\mathcal {L}}^{-1}(U)$ , which is clopen since U is. Clearly f is surjective; for injectivity, suppose $\overline {E_2}(K(x)) \neq \overline {E_2}(K(y))$ . Then

$$\begin{align*}\neg (K(x) \, \overline{E_2} \, K(y)) \rightarrow \neg (x K y) \rightarrow \neg (E_2(x) \, \overline{K} \, E_2(y)), \end{align*}$$

and hence $\overline {K}(E_2(x)) \neq \overline {K}(E_2(y))$ .

Since f is a continuous bijection, it remains to show it preserves and reflects the relations [Reference Esakia, Bezhanishvili and Holliday13, Proposition 1.4.15]. For R, note (checking only the cases where f is not the identity on some input):

• • $K(x) \; R \; E_2(K(y)) \leftrightarrow \widehat {K}(x) \; R \; \widehat {K}(E_2(y))$ (both are always true by definition).

• • $E_2(K(x)) \; R \; E_2(K(y)) \leftrightarrow \widehat {K}(E_2(x)) \; R \; \widehat {K}(E_2(y))$ (similarly).

For E we have

$$\begin{align*}K(x) \; E \; \overline{E_2}(K(y)) \leftrightarrow K(x) \, \overline{E_2} \, K(y) \leftrightarrow x \, E_2 \, y \leftrightarrow x \; E \; E_2(y) \leftrightarrow \widehat{K}(x) \; E \; \widehat{K}(E_2(y)). \end{align*}$$

Thus, f is an isomorphism of $\mathsf {MS4}$ -frames.

Proof. It is sufficient to show that each generator of $\mathfrak {B}$ is $\widehat {K}$ -saturated. Since $\widehat {K}$ relates no points across layers, and each $g_i \cap D_2$ is K-saturated (as a generator of $\mathfrak {B}'$ ), we need only check that $g_i \cap D_1$ is $\overline {K}$ -saturated. Suppose $\alpha \in g_i$ and $\alpha \overline {K} \beta $ . Then there are $x \in \alpha , y \in \beta $ with $x K y$ . Evidently, $x \in E(g_i \cap D_1) \cap D_2$ which is K-saturated (as a generator of $\mathfrak {B}'$ ), so $y \in E(g_i \cap D_1) \cap D_2$ . That is, y is E-related to something in $g_i \cap D_1$ , which could only be $\beta $ , and hence $\beta \in g_i$ .

Proof. Suppose $T(\mathbf {V})$ is locally finite, and let $\mathfrak {A} = \mathfrak {F}^* \in \mathbf {V}_{\text {SI}}$ be generated by $g_1, \dots , g_n$ . Then each $g_i$ is a subset of $D_2 \subseteq T(\mathfrak {F})$ , and by Lemma 6.11 the operations of $\mathfrak {A}_2 \cong \mathfrak {A}$ are definable using the clopen set $D_2$ . By assumption, there is $f:\omega \to \omega $ such that the size of the subalgebra $\langle g_1, \dots , g_n, D_2 \rangle \subseteq T(\mathfrak {A})$ is bounded by $f(n+1)$ . This subalgebra contains every element of $\mathfrak {A}$ . Thus, ${\lvert {\mathfrak {A}} \rvert }\leq f(n+1)$ . By [Reference Bezhanishvili5, Theorem 3.7(4)], we conclude that $\mathbf {V}$ is locally finite.

Suppose $\mathbf {V}$ is locally finite. To prove that $T(\mathbf {V})$ is locally finite, it is sufficient to show that the generating class $\left \{T(\mathfrak {A}) : \mathfrak {A} \in \mathbf {V}_{\text {SI}}\right \}$ is uniformly locally finite (see [Reference Mal’cev, Smirnov and Taĭclin26, p. 285]). Suppose $\mathfrak {B}$ is an n-generated subalgebra of $T(\mathfrak {A})$ , corresponding to a correct partition L of $T(\mathfrak {A}_*)$ . By Lemma 6.13, there is a $2n$ -generated subalgebra $\mathfrak {B}' \subseteq \mathfrak {A}$ such that the corresponding correct partition K of $\mathfrak {A}_*$ satisfies $\widehat {K} \subseteq L$ . Therefore, $\mathfrak {B} \subseteq T(\mathfrak {B}')$ . By assumption, we have $f:\omega \to \omega $ such that ${\lvert {\mathfrak {B}'}\rvert }\leq f(2n)$ . Thus, it follows from Construction 6.8 that the size of $T(\mathfrak {B'})$ and hence of $\mathfrak {B}$ is bounded by $f(2n)^2$ .