Proof. $(1)$ . If $\sigma \mathcal {R}_{\Box _j}\tau $ and $\tau \mathcal {R}_{\Box _i}\upsilon $ , it follows that $\sigma \mathcal {R}_{\Box _i}\upsilon $ , by upward transitivity. But then $\upsilon \mathcal {R}_{\Box _j}\upsilon $ , by downward shift reflexivity. Therefore, there is a sequence $\sigma ^{\prime }$ , namely, $\upsilon $ itself, such that $\sigma \mathcal {R}_{\Box _i}\sigma ^{\prime }$ and $\sigma ^{\prime }\mathcal {R}_{\Box _j}\upsilon $ .

$(2)$ . If $\sigma \mathcal {R}_{\Box _j}\tau $ and $\sigma \mathcal {R}_{\Box _i}\upsilon $ , then $\tau \mathcal {R}_{\Box _i}\upsilon $ , by the upward Euclidean property. But then $\upsilon \mathcal {R}_{\Box _j}\upsilon $ , by downward shift reflexivity. Therefore, there is a sequence $\sigma ^{\prime }$ , namely, $\upsilon $ itself, such that $\tau \mathcal {R}_{\Box _i}\sigma ^{\prime }$ and $\upsilon \mathcal {R}_{\Box _j}\sigma ^{\prime }$ .

Proof. Obviously, $\mathcal {R}_{\Box _i}$ is pseudo-reflexive, since any member of $W^i$ is i-diagonal and identical with itself beyond i. Moreover, it is easy to see that $\mathcal {R}_{\Box _i}$ is pseudo-Euclidean, for if $\sigma \mathcal {R}_{\Box _i}\tau $ and $\sigma \mathcal {R}_{\Box _i}\upsilon $ , then $\sigma $ , $\tau $ , and $\upsilon $ are all identical beyond i, so that $\tau \mathcal {R}_{\Box _i}\upsilon $ as long as $\upsilon \in W^i$ .

Proof. By Theorem 4.42 in Blackburn et al. (Reference Blackburn, de Rijke and Venema2001), the proof of which can be found in chapter 5.

Proof. (1). This is derivable from $\mathbf {AT}_i$ and its dual, $@_i p\rightarrow \Diamond _i p$ .

(2). Consider the following derivation:

$$\begin{align*} \begin{array}{lll} 1.&\vdash_n\Diamond_i p\rightarrow\Box_i\Diamond_i p&\textbf{5}_{\Box_{i}}\\ 2.&\vdash_n\Box_i\Diamond_i p\rightarrow@_i\Diamond_i p&\textbf{AT}_{i}\\ 3.&\vdash_n\Diamond_i p\rightarrow@_i\Diamond_i p&1,2\\ 4.&\vdash_n\neg@_i\neg\Box_i\neg p\rightarrow\Box_i\neg p&3\\ 5.&\vdash_n @_i\Box_i p\rightarrow\Box_i p&\textbf{D}_{@_i},4\\\end{array} \end{align*}$$

$$\begin{align*}\begin{array}{lll} 6.&\vdash_n \Box_j@_i\Box_i p\rightarrow\Box_j\Box_i p&\textbf{Nec}_{\textbf{j}},\textbf{K}_{\Box_j},5\\ 7.&\vdash_n @_i\Box_i p\rightarrow\Box_j@_i\Box_i p&\textbf{A4}_{i}\\ 8.&\vdash_n @_i\Box_i p\rightarrow\Box_j\Box_i p&6,7\\ 9.&\vdash_n \Box_i p\rightarrow\Box_i\Box_i p&\textbf{4}_{\Box_i}\\ 10.&\vdash_n \Box_i\Box_i p\rightarrow@_i\Box_i p&\textbf{AT}_{i}\\ 11.&\vdash_n \Box_i p\rightarrow@_i\Box_i p&9,10\\ 12.&\vdash_n \Box_i p\rightarrow\Box_j\Box_i p&8,11\\ \end{array} \end{align*}$$

(3). Consider the following derivation:

$$ \begin{align*}\begin{array}{lll} 1.&\vdash_n\Box_i\Diamond_i p\rightarrow\Diamond_i\Diamond_i p&(1)\\ 2.&\vdash_n\Diamond_i\Diamond_i p\rightarrow\Diamond_i p&\text{Dual of }\textbf{4}_{\Box_i}\\ 3.&\vdash_n\Box_i\Diamond_i p\rightarrow\Diamond_i p&1,2\\ 4.&\vdash_n \Box_j\Box_i\Diamond_i p\rightarrow\Box_j\Diamond_i p&\textbf{Nec}_{j},3,\textbf{K}_{\Box_j}\\ 5.&\vdash_n \Box_i\Diamond_i p\rightarrow\Box_j\Box_i\Diamond_i p&(2)\\ 6.&\vdash_n \Diamond_i p\rightarrow\Box_i\Diamond_i p&\textbf{5}_{\Box_i}\\ 7.&\vdash_n \Diamond_i p\rightarrow\Box_j\Diamond_i p&4,5,6\\ \end{array}\end{align*} $$

Proof. (1). One inclusion is clear. For the other direction, let

$$\begin{align*}Z=\mathcal{R}^w_{\Box_1}[\mathcal{R}^w_{\Box_2}[\cdots[\mathcal{R}^w_{\Box_i}[\cdots[\mathcal{R}^w_{\Box_n}[\{w\}]]]]]]. \end{align*}$$

We first prove that (1a) $w\in Z$ , and then that (1b) Z is closed under every relation $\mathcal {R}^w_{\mathcal {O}_i}$ in the frame $\mathfrak {F}^w$ .

(1a). Let z be the element in $W^w$ such that $\mathcal {R}^w_{@_n}(w)=z$ , and for each i such that $1\leq i<n$ , let $\mathcal {R}^w_{@_i}(w)=z_i$ and $\mathcal {R}^w_{@_i}(z_i)=v_i$ . Then $w\mathcal {R}^w_{\Box _n}z$ , by $\mathbf {AT}_n$ , and both $w\mathcal {R}^w_{\Box _{n-1}}z_{n-1}$ and $z_{n-1}\mathcal {R}^w_{\Box _{n-1}}v_{n-1}$ , by $\mathbf {AT}_{n-1}$ . So $w\mathcal {R}^w_{\Box _{n-1}}v_{n-1}$ , by transitivity of $\mathcal {R}^w_{\Box _{n-1}}$ . But $w\mathcal {R}^w_{\Box _{n-1}}z$ follows by $\mathbf {A}_n$ , and so $z\mathcal {R}^w_{\Box _{n-1}}v_{n-1}$ , since $\mathcal {R}^w_{\Box _{n-1}}$ is Euclidean. Then

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z\mathcal{R}^w_{\Box_{n-1}}v_{n-1}. \end{align*}$$

Moreover, both $w\mathcal {R}^w_{\Box _{n-2}}z_{n-2}$ and $z_{n-2}\mathcal {R}^w_{\Box _{n-2}}v_{n-2}$ follow by $\mathbf {AT}_{n-2}$ . So $w\mathcal {R}^w_{\Box _{n-2}}v_{n-2}$ , by transitivity of $\mathcal {R}^w_{\Box _{n-2}}$ . Also, both $w\mathcal {R}^w_{\Box _{n-2}}z_{n-1}$ and $z_{n-1}\mathcal {R}^w_{\Box _{n-2}}v_{n-1}$ , by $\mathbf {A}_{n-1}$ . So $w\mathcal {R}^w_{\Box _{n-2}}v_{n-1}$ , again by transitivity of $\mathcal {R}^w_{\Box _{n-2}}$ . Hence $v_{n-1}\mathcal {R}^w_{\Box _{n-2}}v_{n-2}$ , as $\mathcal {R}^w_{\Box _{n-2}}$ is Euclidean. Then

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z\mathcal{R}^w_{\Box_{n-1}}v_{n-1}\mathcal{R}^w_{\Box_{n-2}}v_{n-2}. \end{align*}$$

By repeating this argument multiple times, it follows that there is a chain

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z\mathcal{R}^w_{\Box_{n-1}}v_{n-1}\mathcal{R}^w_{\Box_{n-2}}v_{n-2}\cdots\mathcal{R}^w_{\Box_{3}}v_{3}\mathcal{R}^w_{\Box_{2}}v_{2}. \end{align*}$$

Now, by $\mathbf {A}_{2}$ , both $w\mathcal {R}^w_{\Box _{1}}z_{2}$ and $z_{2}\mathcal {R}^w_{\Box _{1}}v_{2}$ , whence $w\mathcal {R}^w_{\Box _{1}}v_{2}$ and so $v_{2}\mathcal {R}^w_{\Box _{1}}w$ , by transitivity and symmetry of $\mathcal {R}^w_{\Box _{1}}$ , respectively, thereby extending the chain above to

$$\begin{align*}(\ast)\ w{\mathcal{R}}^w_{\Box_n}z{\mathcal{R}}^w_{\Box_{n-1}}v_{n-1}{\mathcal{R}}^w_{\Box_{n-2}}v_{n-2}\cdots{\mathcal{R}}^w_{\Box_{3}}v_{3}{\mathcal{R}}^w_{\Box_{2}}v_{2}{\mathcal{R}}^w_{\Box_{1}}w. \end{align*}$$

Therefore, $w\in Z$ .

(1b). For $\mathcal {R}^w_{\Box _1}$ , suppose that $v\in \mathcal {R}^w_{\Box _1}[Z]$ . Then there is a $u\in Z$ such that $u\mathcal {R}^w_{\Box _1}v$ . But since $u\in Z$ , it follows by an argument similar to that which established $(*)$ in (1a) that there are $z_n,\ldots ,z_2\in W^w$ such that

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z_n\mathcal{R}^w_{\Box_{n-1}}z_{n-1}\mathcal{R}^w_{\Box_{n-2}}z_{n-2}\cdots\mathcal{R}^w_{\Box_{3}}z_{3}\mathcal{R}^w_{\Box_{2}}z_{2}\mathcal{R}^w_{\Box_{1}}u. \end{align*}$$

By transitivity of $\mathcal {R}^w_{\Box _1}$ , it then follows that $z_2\mathcal {R}^w_{\Box _1}v$ , and so $v\in Z$ .

For $\mathcal {R}^w_{\Box _i}$ , where $1<i\leq n$ , suppose that $v\in \mathcal {R}^w_{\Box _i}[Z]$ . Then there is a $u\in Z$ such that $u\mathcal {R}^w_{\Box _i}v$ . But since $u\in Z$ , it follows by an argument similar to the one establishing $(*)$ in (1a), that there are $z_n,\ldots ,z_2\in W^w$ such that

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z_n\mathcal{R}^w_{\Box_{n-1}}z_{n-1}\mathcal{R}^w_{\Box_{n-2}}z_{n-2}\cdots\mathcal{R}^w_{\Box_{3}}z_{3}\mathcal{R}^w_{\Box_{2}}z_{2}\mathcal{R}^w_{\Box_{1}}u. \end{align*}$$

By upward transitivity, it follows that $z_2\mathcal {R}^w_{\Box _i}v$ . Now, if $i=2$ , then $z_{3}\mathcal {R}^w_{\Box _{2}}v$ , by transitivity of $\mathcal {R}^w_{\Box _{2}}$ , from which it follows that $v\in Z$ , as $\mathcal {R}^w_{\Box _1}$ is reflexive. If, on the other hand, $2<i<n$ , since $z_3\mathcal {R}^w_{\Box _2}z_2$ , it follows that $z_3\mathcal {R}^w_{\Box _i}v$ , by upward transitivity; since $z_4\mathcal {R}^w_{\Box _3}z_3$ and $z_3\mathcal {R}^w_{\Box _i}v$ , it follows that $z_4\mathcal {R}^w_{\Box _i}v$ by upward transitivity; after multiple repetitions of this argument, since $z_i\mathcal {R}^w_{\Box _{i-1}}z_{i-1}$ and $z_{i-1}\mathcal {R}^w_{\Box _i}v$ , it follows that $z_i\mathcal {R}^w_{\Box _i}v$ by upward transitivity. Then $v\mathcal {R}^w_{@_i}v$ , by $\mathbf {AR}_i$ , whence $v\mathcal {R}^w_{\Box _{i-1}}v$ , by $\mathbf {A}_i$ , and so $v\mathcal {R}^w_{@_{i-1}}v$ , by $\mathbf {AR}_{i-1}$ , whence $v\mathcal {R}^w_{\Box _{i-2}}v$ , by $\mathbf {A}_{i-1}$ , and so on. After multiple repetitions of this argument, $v\mathcal {R}^w_{@_{3}}v$ , by $\mathbf {AR}_{3}$ , whence $v\mathcal {R}^w_{\Box _{2}}v$ , by $\mathbf {A}_{3}$ . Also $v\mathcal {R}^w_{\Box _{1}}v$ , since $\mathcal {R}^w_{\Box _{1}}$ is reflexive, and so $v\in Z$ . In case $i=n$ , since $w\mathcal {R}^w_{\Box _{n}}z_{n}$ , and $z_{n}\mathcal {R}^w_{\Box _n}v$ follows as in the argument above, it then follows that $w\mathcal {R}^w_{\Box _n}v$ by transitivity of $\mathcal {R}^w_{\Box _n}$ . The rest of the argument for the descending chain is exactly as the case $2<i<n$ above.

For $\mathcal {R}^w_{@_1}$ , suppose that $v\in \mathcal {R}^w_{@_1}[Z]=Z$ , since $\mathcal {R}^w_{@_1}$ is the identity function. So $v\in Z$ .

For $\mathcal {R}^w_{@_i}$ , where $1<i\leq n$ , suppose that $v\in \mathcal {R}^w_{@_i}[Z]$ . Then there is a $u\in Z$ such that $u\mathcal {R}^w_{@_i}v$ . So $u\mathcal {R}^w_{\Box _i}v$ , by $\mathbf {AT}_i$ . That $v\in Z$ now follows from the argument for $\mathcal {R}^w_{\Box _i}$ .

(2). For the left-to-right direction, suppose that $v\mathcal {R}^w_{\Box _n}u$ . By $\mathbf {AR}_n$ , $u\mathcal {R}^w_{@_n}u$ , so $u\in im(\mathcal {R}^w_{@_{n}})$ . For the converse, assume that $u\in im(\mathcal {R}^w_{@_{n}})$ , and let z be the element in $ W^w$ such that $\mathcal {R}^w_{@_{n}}(w)=z$ . Now, consider any point $v\in W^w$ . We show that (2a) $v\mathcal {R}^w_{\Box _n}z$ , and then that (2b) $z\mathcal {R}^w_{\Box _n}u$ , from which $v\mathcal {R}^w_{\Box _n}u$ follows by transitivity of $\mathcal {R}^w_{\Box _n}$ , thereby proving the lemma.

(2a) Since $v\in W^w$ , it follows by an argument similar to the one establishing $(*)$ in (1a) that there are $z_n,\ldots ,z_2\in W^w$ such that

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z_n\mathcal{R}^w_{\Box_{n-1}}z_{n-1}\mathcal{R}^w_{\Box_{n-2}}z_{n-2}\cdots\mathcal{R}^w_{\Box_{3}}z_{3}\mathcal{R}^w_{\Box_{2}}z_{2}\mathcal{R}^w_{\Box_{1}}v. \end{align*}$$

By symmetry of $\mathcal {R}^w_{\Box _1}$ , it follows that $v\mathcal {R}^w_{\Box _1}z_2$ . Now consider $z_3^{\prime }\in \mathcal {R}^w_{@_2}(z_3)$ . By $\mathbf {AT}_2$ , it follows that $z_3\mathcal {R}^w_{\Box _2}z_3^{\prime }$ . So $z_3\mathcal {R}^w_{\Box _2}z_2$ and $z_3\mathcal {R}^w_{\Box _2}z_3^{\prime }$ , from which $z_2\mathcal {R}^w_{\Box _2}z_3^{\prime }$ follows from the Euclidean property of $\mathcal {R}^w_{\Box _2}$ . So $v\mathcal {R}^w_{\Box _1}z_2$ and $z_2\mathcal {R}^w_{\Box _2}z_3^{\prime }$ , hence $v\mathcal {R}^w_{\Box _2}z_3^{\prime }$ , by upward transitivity. Now consider $z_4^{\prime }=\mathcal {R}^w_{@_3}(z_4)$ . By $\mathbf {AT}_3$ , it follows that $z_4\mathcal {R}^w_{\Box _3}z_4^{\prime }$ . So $z_4\mathcal {R}^w_{\Box _3}z_3$ and $z_4\mathcal {R}^w_{\Box _3}z_4^{\prime }$ , from which $z_3\mathcal {R}^w_{\Box _3}z_4^{\prime }$ follows from the Euclidean property of $\mathcal {R}^w_{\Box _3}$ . Since $z_3\mathcal {R}^w_{\Box _2}z_3^{\prime }$ , it follows that $z_3^{\prime }\mathcal {R}^w_{\Box _3}z_4^{\prime }$ , by upward Euclideanity. And since $v\mathcal {R}^w_{\Box _2}z_3^{\prime }$ , it follows that $v\mathcal {R}^w_{\Box _3}z_4^{\prime }$ , by upward transitivity. By repeating this argument multiple times, it follows that $v\mathcal {R}^w_{\Box _{n-1}}z_n^{\prime }$ . Now consider $z=\mathcal {R}^w_{@_n}(w)$ . By $\mathbf {AT}_n$ , it follows that $w\mathcal {R}^w_{\Box _n}z$ . So $w\mathcal {R}^w_{\Box _n}z_n$ and $w\mathcal {R}^w_{\Box _n}z$ , whence $z_n\mathcal {R}^w_{\Box _n}z$ , by the Euclidean property of $\mathcal {R}^w_{\Box _n}$ . Then $z_n\mathcal {R}^w_{\Box _{n-1}}z_n^{\prime }$ (by a previous iteration of the argument) and $z_n\mathcal {R}^w_{\Box _n}z$ , so $z_n^{\prime }\mathcal {R}^w_{\Box _n}z$ follows by upward Euclideanity. Therefore, $v\mathcal {R}^w_{\Box _{n-1}}z_n^{\prime }$ and $z_n^{\prime }\mathcal {R}^w_{\Box _n}z$ , from which $v\mathcal {R}^w_{\Box _n}z$ follows by upward transitivity.

(2b). Since $u\in W^w$ , by hypothesis, it follows by an argument similar to the one establishing $(*)$ in (1a) that there are $z_n,\ldots ,z_2\in W^w$ such that

$$\begin{align*}w\mathcal{R}^w_{\Box_n}z_n\mathcal{R}^w_{\Box_{n-1}}z_{n-1}\mathcal{R}^w_{\Box_{n-2}}z_{n-2}\cdots\mathcal{R}^w_{\Box_{3}}z_{3}\mathcal{R}^w_{\Box_{2}}z_{2}\mathcal{R}^w_{\Box_{1}}u. \end{align*}$$

Consider $z=\mathcal {R}^w_{@_n}(w)$ . Then $w\mathcal {R}^w_{\Box _n}z$ , by $\mathbf {AT}_n$ . Since $\mathcal {R}^w_{\Box _n}$ is Euclidean, it follows that $z\mathcal {R}^w_{\Box _n}z_n$ . Since $u\in im(\mathcal {R}^w_{@_n})$ , there is a $u_n\in W^w$ such that $u_n\mathcal {R}^w_{@_n}u$ . By $\mathbf {AT}_n$ , $u_n\mathcal {R}^w_{\Box _{n}}u$ , whence $u\mathcal {R}^w_{@_{n}}u$ , by $\mathbf {AR}_{n}$ , and so $u\mathcal {R}^w_{\Box _{n}}u$ , by $\mathbf {AT}_{n}$ . By $\mathbf {A}_n$ , in turn, it also follows that $u_n\mathcal {R}^w_{\Box _{n-1}}u$ , so $u\mathcal {R}^w_{@_{n-1}}u$ by $\mathbf {AR}_{n-1}$ , whence $u\mathcal {R}^w_{\Box _{n-2}}u$ by $\mathbf {A}_{n-1}$ . Then $u\mathcal {R}^w_{@_{n-2}}u$ by $\mathbf {AR}_{n-1}$ , whence $u\mathcal {R}^w_{\Box _{n-3}}u$ by $\mathbf {A}_{n-2}$ . By repeating this argument multiple times, it follows that $u\mathcal {R}^w_{\Box _{3}}u$ by $\mathbf {A}_{4}$ and, similarly, that $u\mathcal {R}^w_{\Box _{2}}u$ by $\mathbf {A}_{3}$ . Now, since $z_2\mathcal {R}^w_{\Box _1}u$ and $u\mathcal {R}^w_{\Box _2}u$ , $z_2\mathcal {R}^w_{\Box _2}u$ follows by upward transitivity. And because $z_3\mathcal {R}^w_{\Box _2}z_2$ and $z_2\mathcal {R}^w_{\Box _2}u$ , $z_3\mathcal {R}^w_{\Box _2}u$ follows by transitivity of $\mathcal {R}^w_{\Box _2}$ . But since $z_3\mathcal {R}^w_{\Box _2}u$ and $u\mathcal {R}^w_{\Box _3}u$ , $z_3\mathcal {R}^w_{\Box _3}u$ follows by upward transitivity, and so $z_4\mathcal {R}^w_{\Box _3}u$ follows by transitivity of $\mathcal {R}^w_{\Box _3}$ . By repeating this argument multiple times it follows that $z_n\mathcal {R}^w_{\Box _{n-1}}u$ . But since $u\mathcal {R}^w_{\Box _{n}}u$ , it follows that $z_n\mathcal {R}^w_{\Box _{n}}u$ by upward transitivity. And since $z\mathcal {R}^w_{\Box _n}z_n$ , it follows that $z\mathcal {R}^w_{\Box _n}u$ by transitivity of $\mathcal {R}^w_{\Box _n}$ , as desired.

Proof. Let $\mathcal {R}_{@_{i+1}}(v)=z$ . Then $v\mathcal {R}_{\Box _{i+1}}z$ , by $\mathbf {AT}_{i+1}$ , and so $z\mathcal {R}_{@_{i+1}}z$ follows by $\mathbf {AR}_{i+1}$ . Now $z\mathcal {R}_{\Box _{i}}z$ follows by $\mathbf {A}_{i+1}$ , and $z\mathcal {R}_{@_{i}}z$ follows by $\mathbf {AR}_{i}$ . So $v\mathcal {R}_{@_{i+1}}z\mathcal {R}_{@_{i}}z$ , and hence

$$\begin{align*}\mathcal{R}_{@_{i}}(\mathcal{R}_{@_{i+1}}(v))=\mathcal{R}_{@_{i}}(z)=z=\mathcal{R}_{@_{i+1}}(v), \end{align*}$$

as desired.

Proof. (1). The proof is by induction on $1\leq i\leq (n-1)$ . For $i=1$ , since for any $w_1\in W$ , $\mathcal {R}_{\Box _{n-1}}[g^0_\emptyset (w_1)]\subseteq W$ , and $\mathcal {R}_{@_n}$ is a function such that $\mathcal {R}_{@_n}\subseteq \mathcal {R}_{\Box _{n-1}}$ , by $\mathbf {A}_n$ , there is a family of surjective functions

$$\begin{align*}g^1_{w_1}:W\rightarrow\mathcal{R}_{\Box_{n-1}}[g^{0}_\emptyset(w_1)] \end{align*}$$

such that

$$\begin{align*}g^1_{w_1}(w_1)=\mathcal{R}_{@_n}(g^{0}_\emptyset(w_1)). \end{align*}$$

Assume the induction hypothesis, for $i=k$ , where $1\leq k< (n-1)$ , that there is family of surjective functions

$$\begin{align*}g^{k}_{w_1,\ldots,w_{k}}:W\rightarrow\mathcal{R}_{\Box_{n-k}}[g^{k-1}_{w_2,\ldots,w_{k}}(w_1)] \end{align*}$$

such that

$$\begin{align*}g^{k}_{w_1,\ldots,w_{k}}(w_1)=\mathcal{R}_{@_{n-(k-1)}}(g^{k-1}_{w_2,\ldots,w_k}(w_1)). \end{align*}$$

We show that the lemma holds for $i=k+1$ . Since, by the induction hypothesis, there are functions $g^{k}_{w_1,\ldots ,w_k}$ , and both $\mathcal {R}_{\Box _{n-(k+1)}}[g^{k}_{w_2,\ldots ,w_{k+1}}(w_1)]\subseteq W$ and $\mathcal {R}_{@_{n-k}}\subseteq \mathcal {R}_{\Box _{n-(k+1)}}$ , by $\mathbf {A}_{n-k}$ , it follows that there is a family of surjective functions

$$\begin{align*}g^{k+1}_{w_1,\ldots,w_{k+1}}:W\rightarrow\mathcal{R}_{\Box_{n-(k+1)}}[g^{k}_{w_2,\ldots,w_{k+1}}(w_1)] \end{align*}$$

such that

$$\begin{align*}g^{k+1}_{w_1,\ldots,w_{k+1}}(w_1)=\mathcal{R}_{@_{n-k}}(g^{k}_{w_2,\ldots,w_{k+1}}(w_1)), \end{align*}$$

as desired.

(2). The proof is by induction on j. For $j=1$ , it follows from (1) that

$$\begin{align*}g^{n-1}_{w_1,\ldots,w_{n-1}}(z)=\mathcal{R}_{@_{2}}(g^{n-2 }_{w_2,\ldots,w_{n-1}}(w_1)). \end{align*}$$

Now let $j=k$ , where $1\leq k< (n-1)$ , and assume that

$$\begin{align*}g^{n-1}_{w_1,\ldots,w_{n-1}}(z)=\mathcal{R}_{@_{k+1}}(g^{n-(k+1)}_{w_{k+1},\ldots,w_{n-1}}(w_k)). \end{align*}$$

Suppose that $w_1=\cdots =w_{k+1}=z$ . Then the family of surjections

$$\begin{align*}g^{n-(k+1)}_{w_{k+1},\ldots,w_{n-1}}:W\rightarrow\mathcal{R}_{\Box_{n-(n-(k+1))}}[g^{(n-(k+1))-1}_{w_{k+2},\ldots,w_{n-1}}(w_{k+1})] \end{align*}$$

is such that

$$\begin{align*}g^{n-(k+1)}_{w_{k+1},\ldots,w_{n-1}}(w_k)=\mathcal{R}_{@_{n-((n-(k+1))-1)}}(g^{(n-(k+1))-1}_{w_{k+2},\ldots,w_{n-1}}(w_{k+1})), \end{align*}$$

by (1), and hence

$$\begin{align*}g^{n-1}_{w_1,\ldots,w_{n-1}}(z)=\mathcal{R}_{@_{k+1}}(\mathcal{R}_{@_{n-((n-(k+1))-1)}}(g^{(n-(k+1))-1}_{w_{k+2},\ldots,w_{n-1}}(w_{k+1}))). \end{align*}$$

Note, moreover, that $n-((n-(k+1))-1)=k+2$ , and hence

$$\begin{align*}g^{n-1}_{w_1,\ldots,w_{n-1}}(z)=\mathcal{R}_{@_{n-((n-(k+1))-1)}}(g^{(n-(k+1))-1}_{w_{k+2},\ldots,w_{n-1}}(w_{k+1})), \end{align*}$$

by Lemma 1.3, as desired.

Proof. Let $\mathfrak {F}$ , $w\in W$ , and $\mathfrak {F}^w$ be as in the hypothesis. Because generated subframes preserve validity between frames, all of the $\mathbf {S}@_n$ axioms hold in $\mathfrak {F}^w$ . So in what follows we construct a sequence frame, $\mathfrak {F}^{\prime }=(W^{\prime },(\mathcal {R}^{\prime }_{\Box _i})_{1\leq i\leq n},(\mathcal {R}^{\prime }_{@_i})_{1\leq i\leq n})$ , such that $W^{\prime }=(W^w)^n$ , where $(W^w)^n$ is the n-fold Cartesian product of $W^w$ , and a surjective bounded morphism $f:\mathfrak {F}^{\prime }\twoheadrightarrow \mathfrak {F}^w$ . Then, where $\sigma \in (W^w)^n$ , let $f:(W^w)^n\rightarrow W^w$ be defined as

$$\begin{align*}f(\sigma)=g^{n-1}_{\sigma_2,\ldots,\sigma_n}(\sigma_1), \end{align*}$$

where the sequence $g^0,\ldots ,g^{n-1}$ of families of surjective functions is defined on $W^w$ . We prove that f so defined is a bounded morphism from $\mathfrak {F}^{\prime }$ onto $\mathfrak {F}^w$ by checking the back and forth conditions for each accessibility relation as follows:

$[\mathcal {R}_{\Box _1}]$ Suppose that $\sigma \mathcal {R}^{\prime }_{\Box _1}\sigma ^{\prime }$ . Then $\sigma $ and $\sigma ^{\prime }$ are identical beyond 1. So $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ , and $f(\sigma ^{\prime })=g^{n-1}_{\sigma _2^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _1^{\prime }) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ , from which it follows that $f(\sigma )\mathcal {R}^w_{\Box _1}f(\sigma ^{\prime })$ . Conversely, suppose that $f(\sigma )\mathcal {R}^w_{\Box _1}z$ . Since

$$\begin{align*}f(\sigma)=g^{n-1}_{\sigma_2,\ldots,\sigma_{n}}(\sigma_1) \in\mathcal{R}^w_{\Box_{1}}[g^{n-2}_{\sigma_3,\ldots,\sigma_{n}}(\sigma_2)], \end{align*}$$

it follows that $z\in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . And since $g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}$ is a surjection, there is a $v\in W^w$ such that $g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(v)=z$ , whence $f(\sigma ^1_v)=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(v)=z$ . Furthermore, $\sigma \mathcal {R}^{\prime }_{\Box _1}\sigma ^1_v$ .

$[\mathcal {R}_{\Box _i}, 1<i<n]$ Suppose that $\sigma \mathcal {R}^{\prime }_{\Box _i}\sigma ^{\prime }$ . Then $\sigma ^{\prime }$ is i-diagonal and identical with $\sigma $ beyond i. So $f(\sigma ^{\prime })=g^{n-1}_{\sigma _2^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _1^{\prime })=\mathcal {R}^w_{@_i}(g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime }))$ , by Lemma 1.4(2), and $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . Since $g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime })\mathcal {R}^w_{@_i}f(\sigma ^{\prime })$ , it follows that $g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime })\mathcal {R}^w_{\Box _i}f(\sigma ^{\prime })$ , by $\mathbf {AT}_i$ . Also, $g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime }) \in \mathcal {R}^w_{\Box _{i}}[g^{(n-i)-1}_{\sigma _{i+2},\ldots ,\sigma _{n}}(\sigma _{i+1})]$ , since the sequences $\sigma $ and $\sigma ^{\prime }$ are identical beyond i, whence $g^{(n-i)-1}_{\sigma _{i+2},\ldots ,\sigma _{n}}(\sigma _{i+1})\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ , by transitivity of $\mathcal {R}^w_{\Box _{i}}$ . But

$$ \begin{align*}\begin{array}{llll} g^{n-2}_{\sigma_3,\ldots,\sigma_{n}}(\sigma_2)\in\mathcal{R}^w_{\Box_{2}}[g^{n-3}_{\sigma_4,\ldots,\sigma_{n}}(\sigma_3)],\\ g^{n-3}_{\sigma_4,\ldots,\sigma_{n}}(\sigma_3)\in\mathcal{R}^w_{\Box_{3}}[g^{n-4}_{\sigma_5,\ldots,\sigma_{n}}(\sigma_4)],\\ ...,\\ g^{n-i}_{\sigma_{i+1},\ldots,\sigma_{n}}(\sigma_{i})\in\mathcal{R}^w_{\Box_{i}}[g^{(n-i)-1}_{\sigma_{i+2},\ldots,\sigma_{n}}(\sigma_{i+1})]. \end{array}\end{align*} $$

So $g^{n-i}_{\sigma _{i+1},\ldots ,\sigma _{n}}(\sigma _{i})\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ , by the Euclidean property of $\mathcal {R}^w_{\Box _{i}}$ . Now, $g^{n-(i-1)}_{\sigma _{i},\ldots ,\sigma _{n}}(\sigma _{i-1}) \in \mathcal {R}^w_{\Box _{i-1}}[g^{n-i}_{\sigma _{i+1},\ldots ,\sigma _{n}}(\sigma _{i})]$ . So $g^{n-(i-1)}_{\sigma _{i},\ldots ,\sigma _{n}}(\sigma _{i-1})\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ , by upward Euclideanity. By an analogous argument, since $g^{n-(i-2)}_{\sigma _{i-1},\ldots ,\sigma _{n}}(\sigma _{i-2}) \in \mathcal {R}^w_{\Box _{i-2}}[g^{n-(i-1)}_{\sigma _{i},\ldots ,\sigma _{n}}(\sigma _{i-1})]$ , it follows that $g^{n-(i-2)}_{\sigma _{i-1},\ldots ,\sigma _{n}}(\sigma _{i-2})\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ , by upward Euclideanity. By multiple repetitions of this argument, it follows that $g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ . Since $g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ , by upward Euclideanity, again, it follows that $g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1)\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ , and therefore $f(\sigma )\mathcal {R}^w_{\Box _{i}}f(\sigma ^{\prime })$ . Conversely, suppose that $f(\sigma )\mathcal {R}^w_{\Box _i}z$ . Then $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . So

$$\begin{align*}g^{n-2}_{\sigma_3,\ldots,\sigma_{n}}(\sigma_2)\mathcal{R}^w_{\Box_{1}}f(\sigma)\mathcal{R}^w_{\Box_i}z, \end{align*}$$

from which $g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)\mathcal {R}^w_{\Box _i}z$ follows by upward transitivity. Now, $g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2) \in \mathcal {R}^w_{\Box _{2}}[g^{n-3}_{\sigma _4,\ldots ,\sigma _{n}}(\sigma _3)]$ , whence

$$\begin{align*}g^{n-3}_{\sigma_4,\ldots,\sigma_{n}}(\sigma_3)\mathcal{R}^w_{\Box_{2}}g^{n-2}_{\sigma_3,\ldots,\sigma_{n}}(\sigma_2)\mathcal{R}^w_{\Box_i}z, \end{align*}$$

from which $g^{n-3}_{\sigma _4,\ldots ,\sigma _{n}}(\sigma _3)\mathcal {R}^w_{\Box _i}z$ follows by upward transitivity. Similarly, $g^{n-3}_{\sigma _4,\ldots ,\sigma _{n}}(\sigma _3) \in \mathcal {R}^w_{\Box _{3}}[g^{n-4}_{\sigma _5,\ldots ,\sigma _{n}}(\sigma _4)]$ , whence

$$\begin{align*}g^{n-4}_{\sigma_5,\ldots,\sigma_{n}}(\sigma_4)\mathcal{R}^w_{\Box_{3}}g^{n-3}_{\sigma_4,\ldots,\sigma_{n}}(\sigma_3)\mathcal{R}^w_{\Box_i}z, \end{align*}$$

from which $g^{n-4}_{\sigma _5,\ldots ,\sigma _{n}}(\sigma _4)\mathcal {R}^w_{\Box _i}z$ follows by upward transitivity. By repeating this argument, $g^{n-i}_{\sigma _{i+1},\ldots ,\sigma _{n}}(\sigma _{i})\mathcal {R}^w_{\Box _{i}}z$ , but since $g^{n-i}_{\sigma _{i+1},\ldots ,\sigma _{n}}(\sigma _{i}) \in \mathcal {R}^w_{\Box _{i}}[g^{(n-i)-1}_{\sigma _{i+2},\ldots ,\sigma _{n}}(\sigma _{i+1})]$ , it follows that

$$\begin{align*}g^{(n-i)-1}_{\sigma_{i+2},\ldots,\sigma_{n}}(\sigma_{i+1})\mathcal{R}^w_{\Box_{i}}g^{n-i}_{\sigma_{i+1},\ldots,\sigma_{n}}(\sigma_{i})\mathcal{R}^w_{\Box_{i}}z, \end{align*}$$

and so $g^{(n-i)-1}_{\sigma _{i+2}...\sigma _{n}}(\sigma _{i+1})\mathcal {R}^w_{\Box _{i}}z$ follows by transitivity of $\mathcal {R}^w_{\Box _{i}}$ . Then $z\in \mathcal {R}^w_{\Box _{i}}[g^{(n-i)-1}_{\sigma _{i+2},\ldots ,\sigma _{n}}(\sigma _{i+1})]$ . Now, since $g^{n-i}_{\sigma _{i+1},\ldots ,\sigma _{n}}$ is a surjective function, it follows that there is a $v\in W^w$ such that

$$\begin{align*}(*)\ g^{n-i}_{\sigma_{i+1}...\sigma_{n}}(v)=z. \end{align*}$$

So consider the i-diagonal sequence $(v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n})\in (W^w)^n$ , which is identical with $\sigma $ beyond i. Then $\sigma \mathcal {R}^{\prime }_{\Box _{i}}(v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n})$ , and so:

$$ \begin{align*}\begin{array}{llll} f((v,\ldots,v,\sigma_{i+1},\ldots,\sigma_{n}))&=&g^{n-1}_{v,\ldots,v,\sigma_{i+1},\ldots,\sigma_{n}}(v)&\text{[by def. of } f]\\ &=&\mathcal{R}^w_{@_{i}}(g^{n-i}_{\sigma_{i+1},\ldots,\sigma_{n}}(v))&\text{[by Lemma 1.4(2)]}\\ &=&\mathcal{R}^w_{@_{i}}(z).&\text{[by } (*)]\\ \end{array}\end{align*} $$

So $z\mathcal {R}^w_{@_{i}}\,f((v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n}))$ , whence $z\mathcal {R}^w_{\Box _{i}}\,f((v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n}))$ , by $\mathbf {AT}_i$ . Then $f(\sigma )\mathcal {R}^w_{\Box _{i}}\,f((v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n}))$ follows by transitivity of $\mathcal {R}^w_{\Box _{i}}$ . Furthermore, $z\mathcal {R}^w_{@_{i}}z$ follows from the original hypothesis and $\mathbf {AR}_i$ , in which case both $z\mathcal {R}^w_{@_{i}}\,f((v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n}))$ and $z\mathcal {R}^w_{@_{i}}z$ , from which $f((v,\ldots ,v,\sigma _{i+1},\ldots ,\sigma _{n}))=z$ follows by $\mathbf {F}_{@_i}$ , as desired.

$[\mathcal {R}_{\Box _{n}}]$ Suppose that $\sigma \mathcal {R}^{\prime }_{\Box _{n}}\sigma ^{\prime }$ . So $\sigma ^{\prime }$ is n-diagonal. Then $f(\sigma ^{\prime })=g^{n-1}_{\sigma _2^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _1^{\prime })=\mathcal {R}^w_{@_{n}}(\sigma _n^{\prime })$ , by Lemma 1.4(2), whence $f(\sigma ^{\prime })\in im(\mathcal {R}^w_{@_{n}})$ . It follows that $f(\sigma )\mathcal {R}^w_{\Box _{n}}f(\sigma ^{\prime })$ , by Lemma 1.2(2). Conversely, suppose that $f(\sigma )\mathcal {R}^w_{\Box _{n}}z$ . So $z\mathcal {R}^w_{@_{n}}z$ , by $\mathbf {AR}_n$ , in which case there is a $v\in W^w$ , namely, u, such that

1. (⋆) $\mathcal {R}^w_{@_{n}}(v)=z$ ,

as $\mathcal {R}^w_{@_{n}}$ is a function. Now consider the sequence $\sigma ^{n}_v\in (W^w)^n$ . Then:

$$ \begin{align*}\begin{array}{llll} f(\sigma^{n}_v)&=&g^{n-1}_{v,\ldots,v}(v)&\text{[by def. of } f]\\ &=&\mathcal{R}^w_{@_{n}}(v)&\text{[by Lemma 1.4(2)]}\\ &=&z.&\text{[by } (\star)]\\ \end{array}\end{align*} $$

Additionally, $\sigma \mathcal {R}^{\prime }_{\Box _{n}}\sigma ^{n}_v$ .

$[\mathcal {R}_{@_{1}}]$ Suppose that $\sigma \mathcal {R}^{\prime }_{@_{1}}\sigma ^{\prime }$ . Then $\sigma =\sigma ^{\prime }$ . Since $\mathcal {R}^w_{@_{1}}$ is reflexive, it follows that $f(\sigma )\mathcal {R}^w_{@_{1}}f(\sigma ^{\prime })$ . Now suppose that $f(\sigma )\mathcal {R}^w_{@_{1}}z$ . Because $\mathcal {R}^w_{@_{1}}$ is reflexive, $f(\sigma )\mathcal {R}^w_{@_{1}}f(\sigma )$ , hence $f(\sigma )=z$ , as $\mathcal {R}^w_{@_{1}}$ is a function. Also, $\sigma \mathcal {R}^{\prime }_{@_{1}}\sigma $ .

$[\mathcal {R}_{@_{i}}, 1<i<n]$ Suppose that $\sigma \mathcal {R}^{\prime }_{@_{i}}\sigma ^{\prime }$ . Then $\sigma ^{\prime }$ is i-diagonal and identical with $\sigma $ beyond $i-1$ . So

$$\begin{align*}f(\sigma^{\prime})=g^{n-1}_{\sigma_2^{\prime},\ldots,\sigma_{n}^{\prime}}(\sigma_1^{\prime})=\mathcal{R}^w_{@_i}(g^{n-i}_{\sigma_{i+1}^{\prime},\ldots,\sigma_{n}^{\prime}}(\sigma_{i}^{\prime})), \end{align*}$$

by Lemma 1.4(2), and $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . Then $f(\sigma )\mathcal {R}^w_{\Box _{1}}g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)$ , by symmetry of $\mathcal {R}^w_{\Box _{1}}$ . Also,

$$ \begin{align*}\begin{array}{llll} g^{n-2}_{\sigma_3,\ldots,\sigma_{n}}(\sigma_2)\in\mathcal{R}^w_{\Box_{2}}[g^{n-3}_{\sigma_4,\ldots,\sigma_{n}}(\sigma_3)],\\ g^{n-3}_{\sigma_4,\ldots,\sigma_{n}}(\sigma_3)\in\mathcal{R}^w_{\Box_{3}}[g^{n-4}_{\sigma_5,\ldots,\sigma_{n}}(\sigma_4)],\\ \ldots,\\ g^{n-(i-1)}_{\sigma_i,\ldots,\sigma_{n}}(\sigma_{i-1})\in\mathcal{R}^w_{\Box_{i-1}}[g^{n-i}_{\sigma_{i+1},\ldots,\sigma_{n}}(\sigma_{i})]. \end{array}\end{align*} $$

Now, since $\sigma ^{\prime }$ is identical with $\sigma $ beyond $i-1$ , it also follows that $g^{n-(i-1)}_{\sigma _i,\ldots ,\sigma _{n}}(\sigma _{i-1}) \in [g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime })]_{\mathcal {R}^w_{\Box _{i-1}}}$ . And since $g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime })\mathcal {R}^w_{@_i}f(\sigma ^{\prime })$ , it follows that $g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime }) \mathcal {R}^w_{\Box _{i-1}}f(\sigma ^{\prime })$ , by $\mathbf {A}_i$ , and so

$$\begin{align*}g^{n-(i-1)}_{\sigma_i,\ldots,\sigma_{n}}(\sigma_{i-1})\mathcal{R}^w_{\Box_{i-1}}f(\sigma^{\prime}), \end{align*}$$

as $\mathcal {R}^w_{\Box _{i-1}}$ is Euclidean. But since $g^{n-(i-2)}_{\sigma _{i-1},\ldots ,\sigma _{n}}(\sigma _{i-2}) \in \mathcal {R}^w_{\Box _{i-2}}[g^{n-(i-1)}_{\sigma _i,\ldots ,\sigma _{n}}(\sigma _{i-1})]$ , it follows that $g^{n-(i-2)}_{\sigma _{i-1},\ldots ,\sigma _{n}}(\sigma _{i-2})\mathcal {R}^w_{\Box _{i-1}}f(\sigma ^{\prime })$ , by upward Euclideanity. And since $g^{n-(i-3)}_{\sigma _{i-2},\ldots ,\sigma _{n}}(\sigma _{i-3}) \in \mathcal {R}^w_{\Box _{i-3}}[g^{n-(i-2)}_{\sigma _{i-1}...\sigma _{n}}(\sigma _{i-2})]$ , it follows that

$$\begin{align*}g^{n-(i-3)}_{\sigma_{i-2},\ldots,\sigma_{n}}(\sigma_{i-3})\mathcal{R}^w_{\Box_{i-1}}f(\sigma^{\prime}), \end{align*}$$

again by upward Euclideanity. By repeating this argument, it follows that $g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)\mathcal {R}^w_{\Box _{i-1}}f(\sigma ^{\prime })$ , by upward Euclideanity. Then $f(\sigma )\mathcal {R}^w_{\Box _{i-1}}f(\sigma ^{\prime })$ , follows from upward Euclideanity, too. But since $g^{n-i}_{\sigma _{i+1}^{\prime },\ldots ,\sigma _{n}^{\prime }}(\sigma _{i}^{\prime })\mathcal {R}^w_{@_i}f(\sigma ^{\prime })$ , it follows that $f(\sigma ^{\prime })\mathcal {R}^w_{@_i}f(\sigma ^{\prime })$ , by $\mathbf {AT}_i$ and $\mathbf {AR}_i$ , respectively. So $f(\sigma )\mathcal {R}^w_{@_i}f(\sigma ^{\prime })$ , by $\mathbf {A4}_i$ . Conversely, suppose that $f(\sigma )\mathcal {R}^w_{@_{i}}z$ . Consider the sequence $\sigma ^{\prime }\in (W^w)^n$ such that $\sigma ^{\prime }$ is i-diagonal and identical with $\sigma $ beyond $i-1$ . Then $\sigma \mathcal {R}^{\prime }_{@_i}\sigma ^{\prime }$ . So

$$\begin{align*}f(\sigma^{\prime})=g^{n-1}_{\sigma_2^{\prime},\ldots,\sigma_{n}^{\prime}}(\sigma_1^{\prime})=\mathcal{R}^w_{@_i}(g^{n-i}_{\sigma_{i+1}^{\prime},\ldots,\sigma_{n}^{\prime}}(\sigma_{i}^{\prime})), \end{align*}$$

by Lemma 1.4(2), and $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . By the same argument as in the forth direction, it follows that $f(\sigma )\mathcal {R}^w_{@_i}f(\sigma ^{\prime })$ . But since $f(\sigma )\mathcal {R}^w_{@_{i}}z$ , by assumption, it follows that $f(\sigma ^{\prime })=z$ , by $\mathbf {F}_{@_i}$ .

$[\mathcal {R}_{@_{n}}]$ Suppose that $\sigma \mathcal {R}^{\prime }_{@_{n}}\sigma ^{\prime }$ . Then $\sigma ^{\prime }$ is n-diagonal and identical with $\sigma $ beyond $(n-1)$ . So

$$\begin{align*}f(\sigma^{\prime})=g^{n-1}_{\sigma_2^{\prime},\ldots,\sigma_{n}^{\prime}}(\sigma_1^{\prime})=\mathcal{R}^w_{@_{n}}(\sigma^{\prime}_n), \end{align*}$$

by Lemma 1.4(2), and $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . Since $\sigma _n=\sigma _n^{\prime }$ , it follows that $\sigma _n\mathcal {R}^w_{@_{n}}f(\sigma ^{\prime })$ , and so both $\sigma _n\mathcal {R}^w_{\Box _{n-1}}f(\sigma ^{\prime })$ , by $\mathbf {A}_n$ , and $f(\sigma ^{\prime })\mathcal {R}^w_{@_{n}}f(\sigma ^{\prime })$ , by $\mathbf {AR}_n$ . Now, $g^{1}_{\sigma _{n}}(\sigma _{n-1}) \in \mathcal {R}^w_{\Box _{n-1}}[\{\sigma _n\}]$ , so it follows that $g^{1}_{\sigma _{n}}(\sigma _{n-1})\mathcal {R}^w_{\Box _{n-1}}f(\sigma ^{\prime })$ , as $\mathcal {R}^w_{\Box _{n-1}}$ is Euclidean. Also, $g^{2}_{\sigma _{n-1},\sigma _{n}}(\sigma _{n-2}) \in \mathcal {R}^w_{\Box _{n-2}}[g^{1}_{\sigma _{n}}(\sigma _{n-1})]$ . So $g^{2}_{\sigma _{n-1},\sigma _{n}}(\sigma _{n-2})\mathcal {R}^w_{\Box _{n-1}}f(\sigma ^{\prime })$ by upward Euclideanity. Analogously,

$$\begin{align*}g^{3}_{\sigma_{n-2},\sigma_{n-1},\sigma_{n}}(\sigma_{n-3}) \in\mathcal{R}^w_{\Box_{n-3}}[g^{2}_{\sigma_{n-1},\sigma_{n}}(\sigma_{n-2})]. \end{align*}$$

So $g^{3}_{\sigma _{n-2},\sigma _{n-1},\sigma _{n}}(\sigma _{n-3})\mathcal {R}^w_{\Box _{n-1}}f(\sigma ^{\prime })$ , again by upward Euclideanity. By repetitions of this argument, it follows that $g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)\mathcal {R}^w_{\Box _{n-1}}f(\sigma ^{\prime })$ , by upward Euclideanity. Since $f(\sigma )\mathcal {R}^w_{\Box _{1}}g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)$ , by symmetry of $\mathcal {R}^w_{\Box _{1}}$ , it follows that $f(\sigma )\mathcal {R}^w_{\Box _{n-1}}f(\sigma ^{\prime })$ , by upward transitivity. Therefore, $f(\sigma )\mathcal {R}^w_{@_{n}}f(\sigma ^{\prime })$ , by $\mathbf {A4}_n$ . Conversely, suppose that $f(\sigma )\mathcal {R}^w_{@_{n}}z$ . Now consider the sequence $\sigma ^{\prime }\in (W^w)^n$ such that $\sigma ^{\prime }$ is n-diagonal and identical with $\sigma $ beyond $n-1$ . Also $\sigma \mathcal {R}^{\prime }_{@_{n}}\sigma ^{\prime }$ . So

$$\begin{align*}f(\sigma^{\prime})=g^{n-1}_{\sigma_2^{\prime},\ldots,\sigma_{n}^{\prime}}(\sigma_1^{\prime})=\mathcal{R}^w_{@_{n}}(\sigma^{\prime}_n), \end{align*}$$

by Lemma 1.4(2), and $f(\sigma )=g^{n-1}_{\sigma _2,\ldots ,\sigma _{n}}(\sigma _1) \in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{\sigma _3,\ldots ,\sigma _{n}}(\sigma _2)]$ . By the same argument as in the forth direction, it follows that $f(\sigma )\mathcal {R}^w_{@_n}f(\sigma ^{\prime })$ . But since $f(\sigma )\mathcal {R}^w_{@_{n}}z$ , it follows that $f(\sigma ^{\prime })=z$ , by $\mathbf {F}_{@_n}$ .

This concludes the back and forth cases. It remains to show that f is surjective. Consider any $u\in W^w$ . By Lemma 1.2(1),

$$\begin{align*}u\in\mathcal{R}^w_{\Box_1}[\mathcal{R}^w_{\Box_2}[...[\mathcal{R}^w_{\Box_i}[...[\mathcal{R}^w_{\Box_n}[\{w\}]]]]]], \end{align*}$$

so there are elements $v_n,\ldots ,v_2\in W^w$ , and a chain

$$\begin{align*}w\mathcal{R}^w_{\Box_n}v_n\mathcal{R}^w_{\Box_{n-1}}v_{n-1}\mathcal{R}^w_{\Box_{n-2}}v_{n-2}\cdots\mathcal{R}^w_{\Box_{3}}v_{3}\mathcal{R}^w_{\Box_{2}}v_{2}\mathcal{R}^w_{\Box_{1}}u. \end{align*}$$

Consider the mapping $g^1_{v_n}:W^w\rightarrow \mathcal {R}^w_{\Box _{n-1}}[\{v_n\}]$ . As this is surjective, and $v_{n-1}\in \mathcal {R}^w_{\Box _{n-1}}[\{v_n\}]$ , there is a $z_{n-1}\in W^w$ such that $g^1_{v_n}(z_{n-1})=v_{n-1}$ . Now consider the mapping $g^2_{z_{n-1},v_n}:W^w\rightarrow \mathcal {R}^w_{\Box _{n-2}}[g^1_{v_n}(z_{n-1})]$ . As this is surjective, and $v_{n-2}\in \mathcal {R}^w_{\Box _{n-2}}[g^1_{v_n}(z_{n-1})]$ , there is a $z_{n-2}\in W^w$ such that $g^2_{z_{n-1},v_n}(z_{n-2})=v_{n-2}$ . After multiple repetitions of this argument, consider the mapping $g^{n-1}_{z_2,\ldots ,z_{n-1},v_n}:W^w\rightarrow \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{z_3,\ldots ,z_{n-1},w}(z_2)]$ . By a previous iteration of the argument, $g^{n-2}_{z_3,\ldots ,z_{n-1},v_n}(z_2)=v_2$ , and so $u\in \mathcal {R}^w_{\Box _{1}}[g^{n-2}_{z_3,\ldots ,z_{n-1},v_n}(z_2)]$ . As $g^{n-1}_{z_2,\ldots ,z_{n-1},v_n}$ is also surjective, there is a $z_{1}\in W^w$ such that $g^{n-1}_{z_2,\ldots ,z_{n-1},v_n}(z_{1})=u$ . Therefore, there is a sequence $(z_1,z_2,\ldots ,z_{n-1},v_n)\in (W^w)^n$ such that

$$\begin{align*}f((z_1,z_2,\ldots,z_{n-1},v_n))=g^{n-1}_{z_2,\ldots,v_n}(z_{1})=u, \end{align*}$$

as desired.

Proof. Soundness is clear given the correspondence between the axioms of $\mathbf {S}@_n$ and the properties of n-dimensional sequence frames. For strong completeness, by Theorem 1.1, $\mathbf {S}@_n$ is strongly complete with respect to the class of $\mathbf {S}@_n$ -frames, that is, $\textsf{F}_{\mathbf {S}@_n}$ . So it suffices to prove that a set of formulas is satisfiable in a sequence frame if and only if it is satisfiable in an $\mathbf {S}@_n$ -frame. Suppose that a set of formulas $\Gamma $ is satisfiable in a sequence frame $\mathfrak {F}\in \textsf{F}$ . Because every sequence frame is an $\mathbf {S}@_n$ -frame, it follows that $\Gamma $ is also satisfiable in an $\mathbf {S}@_n$ -frame. Conversely, suppose that $\Gamma $ is satisfiable in an $\mathbf {S}@_n$ -frame, say, $\mathfrak {F}$ . Then $\Gamma $ is satisfiable in a model $\mathfrak {M}=(W,(\mathcal {R}_{\Box _i})_{1\leq i\leq n},(\mathcal {R}_{@_i})_{1\leq i\leq n},V)$ based on $\mathfrak {F}$ . So there is a point w in $\mathfrak {M}$ such that $\mathfrak {M},w\vDash \Gamma $ . Let $\mathfrak {M}^w=(W^w,(\mathcal {R}^w_{\Box _i})_{1\leq i\leq n},(\mathcal {R}^w_{@_i})_{1\leq i\leq n},V^w)$ be the submodel of $\mathfrak {M}$ generated by w. Since modal satisfaction is invariant under taking generated submodels, and $w\in W^w$ , it follows that $\mathfrak {M}^w,w\vDash \Gamma $ , and so $\Gamma $ is satisfiable in the point-generated subframe $\mathfrak {F}^w$ of $\mathfrak {F}$ . But, by Lemma 1.5, $\mathfrak {F}^w$ is a bounded morphic image of a sequence frame, say, $\mathfrak {F}^{\prime }=(W^{\prime },(\mathcal {R}^{\prime }_{\Box _i})_{1\leq i\leq n},(\mathcal {R}^{\prime }_{@_i})_{1\leq i\leq n})$ . Let $f:\mathfrak {F}^{\prime }\twoheadrightarrow \mathfrak {F}^w$ be a surjective bounded morphism from $\mathfrak {F}^{\prime }$ onto $\mathfrak {F}^w$ , and $\mathfrak {M}^{\prime }=(W^{\prime },(\mathcal {R}^{\prime }_{\Box _i})_{1\leq i\leq n},(\mathcal {R}^{\prime }_{@_i})_{1\leq i\leq n},V^{\prime })$ a model based on $\mathfrak {F}^{\prime }$ such that for each $p\in \textsf{PROP}$ , $V^{\prime }(p)=\{\sigma \in W^{\prime }\mid f(\sigma )\in V^w(p)\}$ . Because f is surjective, and $w\in W^w$ , let $\sigma ^{\prime }$ be a sequence in $W^{\prime }$ such that $f(\sigma ^{\prime })=w$ . Then $\mathfrak {M}^w,f(\sigma ^{\prime })\vDash \Gamma $ . But as $\mathfrak {M}^w$ is a bounded morphic image of $\mathfrak {M}^{\prime }$ , this implies that $\mathfrak {M}^{\prime },\sigma ^{\prime }\vDash \Gamma $ , since modal satisfaction is invariant under bounded morphisms between models. Therefore, $\Gamma $ is satisfiable in the sequence frame $\mathfrak {F}^{\prime }$ .

Proof. Suppose $\varphi $ has a tableau proof, in which case there is a closed tableau, $\mathcal {T}$ , beginning with $[\neg \varphi ]\mathtt{s}$ , where $\mathtt{s}$ is the sequence $(1,2,\ldots ,n)$ . For a contradiction, assume that $\varphi $ is not valid. Thus, there is an n-dimensional sequence model $\mathfrak {M}=(W,(\mathcal {R}_{\Box _i})_{1\leq i\leq n},(\mathcal {R}_{@_i})_{1\leq i\leq n},V)$ , where $W=S^n$ , for some non-empty set S, such that $\mathfrak {M},\sigma \nvDash \varphi $ for some sequence $\sigma \in W$ . Define a function f such that for each $\mathtt{s}_i\in \mathtt{s}$ and $\sigma _i\in \sigma $ , $f(\mathtt{s}_i)=\sigma _i$ , such that $g(\mathtt{s})=(f(\mathtt{s}_1),\ldots ,f(\mathtt{s}_n))=\sigma $ . Then $\{[\neg \varphi ]\mathtt{s}\}$ is satisfiable in $\mathfrak {M}$ . Moreover, since the one point tableau $[\neg \varphi ]\mathtt{s}$ is satisfiable in $\mathfrak {M}$ , $\mathcal {T}$ is also satisfiable in $\mathfrak {M}$ , by Lemma 2.1. Therefore, $\mathcal {T}$ is both closed and satisfiable, which is impossible, whence $\mathfrak {M},\sigma \vDash \varphi $ , as desired.