Convention 3.1. Since $\mathbf {K}\oplus \Phi $ frames are closed under point-generated subframes, which are rooted by definition, we henceforth assume that pointed frames $(W,R,r)$ are rooted at r.

Proof. Let $\Diamond ^mp\to \Diamond ^np\in \Phi $ be arbitrary and suppose $xR_{i}y_1R_i\cdots R_i y_{m-1}R_{i}z$ . By the forth clause, we get that $f_{i}(x)Rf_{i}(y_1)R\cdots R f_{i}(y_{m-1})Rf_{i}(z)$ . So as $(W, R)$ is a $\mathbf {K}\oplus \Phi $ frame, there must be $w_1,\ldots , w_{n-1}\in W$ s.t. $f_{i}(x)Rw_1R\cdots Rw_{n-1}Rf_{i}(z)$ . Applying the back clause $n-1$ times, we additionally find $v_1,\ldots , v_{n-1}\in W_{i}$ s.t. $xR_{i}v_1R_i\cdots R_{i}v_{n-1}$ and $f_{i}(v_{j})=w_j$ , for all $j\in \{1,\ldots , n-1\}$ . This proves (a).

Consequently, defining $W_{i+1}, R_{i+1}$ , and $f_{i+1}$ by adding fresh points $u_{1},\ldots , u_{n-1}$ as in the lemma statement, it only remains to show that $f_{i+1}$ is a p-morphism such that

$$\begin{align*}\text{d}_{i+1}(u_j)=\text{d}_{i+1}(x)+j\text{ for all } j\in \{1,\ldots, n-1\}, \end{align*}$$

and

$$\begin{align*}\text{d}_{i+1}(y)=\text{d}_{i}(y) \text{ for all } y\in W_{i}. \end{align*}$$

We begin with showing that $f_{i+1}$ is a p-morphism. Observe that $f_{i+1}(r_i)= f_i(r_i)=r$ , since $f_i$ is a pointed p-morphism. For the forth condition, assume $aR_{i+1}b$ . We prove that $f_{i+1}(a)Rf_{i+1}(b)$ by cases.

• • If $(a,b)\in R_{i}$ , then forth for $f_{i}$ gives us $f_{i+1}(a)=f_{i}(a)Rf_{i}(b)=f_{i+1}(b)$ .

• • If $(a,b)\in \{(x,u_1), \ldots ,(u_{j}, u_{j+1}), \ldots ,(u_{n-1}, z)\}$ , then $f_{i+1}(a)Rf_{i+1}(b)$ follows because $f_{i}(x)Rw_1R\cdots Rw_{n-1}Rf_{i}(z)$ .

• • If $(a,b)=(u_{j}, c)$ for $c\in W_{i}$ s.t. $v_{j}R_{i}c$ , then the claim follows by forth for $f_{i}$ because $f_{i+1}(u_{j})=w_j=f_{i}(v_{j})Rf_{i}(c)=f_{i+1}(c)$ .

For the back condition, suppose $f_{i+1}(a)Rb'$ . If $a\in W_{i}$ , then $f_{i}(a)=f_{i+1}(a)Rb'$ , so by the back condition for $f_{i}$ , there is $b\in W_{i}$ s.t. $aR_{i}b$ and $f_{i}(b)=b'$ , hence also $aR_{i+1}b$ and $f_{i+1}(b)=f_{i}(b)=b'$ . If $a\notin W_{i}$ , so $a=u_{j}$ , then $f_{i}(v_{j})=w_j=f_{i+1}(u_{j})Rb'$ , so by the back condition for $f_{i}$ , there is $b\in W_{i}$ s.t. $f_{i}(b)=b'$ and $v_{j}R_{i}b$ . But then $u_{j}R_{i+1}b$ and $f_{i+1}(b)=f_{i}(b)=b'$ . Thus, $f_{i+1}$ meets the back condition, and we may therefore conclude that it is a p-morphism.

Lastly, we have to show that $\text {d}_{i+1}(u_j)=\text {d}_{i+1}(x)+j$ and $\text {d}_{i+1}(y)=\text {d}_{i}(y)$ for all $y\in W_{i}$ . To begin, observe that $(W_{i+1}, R_{i+1})$ is rooted at $r_{i}$ , hence $\text {d}_{i+1}(y)$ is well-defined for all $y\in W_{i+1}$ . Now to see that $\text {d}_{i+1}(u_j)=\text {d}_{i+1}(x)+j$ , note that all paths from $r_{i}$ to $u_{1}$ must start with an $R_{i}$ -path to x and end with $(x,u_{1})\in R_{i+1}$ ; similarly, paths to $u_{j+1}$ must start with an $R_{i+1}$ -path to $u_{j}$ and end with $(u_{j},u_{j+1})\in R_{i+1}$ . We thus obtain

$$\begin{align*}\text{d}_{i+1}(u_j)=\text{d}_{i+1}(x)+j,\quad \text{along with}\quad \text{d}_{i+1}(x)=\text{d}_{i}(x). \end{align*}$$

We still need to verify that $\text {d}_{i+1}(y)=\text {d}_{i}(y)$ for all $y\in W_{i}$ . For convenience, write $u_0\mathrel {:=}x$ and $u_n\mathrel {:=}z$ , and observe that for each $j\in \{1,\ldots , n-1\}$ ,

$$ \begin{align*} &\text{d}_{i}(v_{j})\leq \text{d}_{i}(x)+j =\text{d}_{i+1}(u_{j}),\\ &R_{i+1}[u_{j}]\setminus\{u_{j+1}\}\subseteq R_{i}[v_{j}]. \end{align*} $$

This suffices because then for any $R_{i+1}$ -path (starting at $r_i$ ):

• • if it contains $(u_{n-1},u_n)\in R_{i+1}$ , then there is a not longer $R_{i}$ -path to $u_n=z$ as $xR_{i}y_1R_i\cdots R_i y_{m-1}R_{i}z$ implies that

  $$\begin{align*}\text{d}_{i}(z)\leq \text{d}_{i}(x)+m=\text{d}_{i+1}(u_m)\leq \text{d}_{i+1}(u_{n-1});\end{align*}$$

• • if it contains $(u_{j},u_{j+1})\in R_{i+1}$ for $j<n-1$ followed by $(u_{j+1},a)\in R_{i+1}$ for $a\neq u_{j+2}$ , then there is a not longer $R_{i}$ -path to a as $\text {d}_{i}(v_{j+1})\leq \text {d}_{i+1}(u_{j+1})$ and $R_{i+1}[u_{j+1}]\setminus \{u_{j+2}\}\subseteq R_{i}[v_{j+1}]$ implies $v_{j+1}R_{i}a$ .

Thus $\text {d}_{i+1}(y)=\text {d}_i(y)$ for all $y\in W_i$ , which concludes the proof of the lemma.

Proof. Define $W_{i+1}, R_{i+1}$ , and $f_{i+1}$ by adding a point $u\notin W_i$ as in the lemma statement. Both that $f_{i+1}$ is a p-morphism and that

$$\begin{align*}\text{d}_{i+1}(u)=\text{d}_{i+1}(w)+1\quad \text{and}\quad \text{d}_{i+1}(y)=\text{d}_{i}(y) \text{ for all } y\in W_{i} \end{align*}$$

follow by simplified versions of the corresponding arguments from the preceding lemma.

Proof of the Representation Lemma 2.6.

If $\varphi $ is satisfiable in a $\mathbf {K}\oplus \Phi $ frame, then as $\mathbf {K}\oplus \Phi $ frames are closed under point-generated subframes, $\varphi $ is satisfiable at a root of a $\mathbf {K}\oplus \Phi $ frame.

It therefore suffices to show that for every $\mathbf {K}\oplus \Phi $ frame $(W,R,r)$ , there are a frame $(W', R', r')$ and a pointed p-morphism $f:(W',R',r') \to (W,R,r)$ satisfying (2) and

(3) $$ \begin{align} \forall x,y\big(xR'y\to \exists y'[xR'y',\; \text{d}_{r'}(y')=\text{d}_{r'}(x)+1,\; f(y')= f(y)]\big). \end{align} $$

This suffices by Fact 2.5, because for any model $\mathfrak {M}=(W,R,V)$ over $(W,R)$ , defining $V'(p)\mathrel {:=}f^{-1}[V(p)]$ yields a model $\mathfrak {M}'=(W',R', V')$ over $(W',R')$ such that ${r'\sim f(r')=r}$ , and $f(y')=f(y)$ implies $y'\sim y$ .

Accordingly, let $(W,R,r)$ be a rooted $\mathbf {K}\oplus \Phi $ frame. We may assume without loss of generality that $|W|\leq \aleph _0$ : the frame conditions for $\mathbf {K}\oplus \Phi $ are first-order and $\Phi $ is countable, so it follows by Löwenheim–Skolem through the standard translation that $\mathbf {K}\oplus \Phi $ has the countable model property.Footnote ³

We construct $(W', R', r')$ and f step by step, applying the preceding lemmas iteratively.

First, we set $(W_0, R_0,r_0)\mathrel {:=}(W,R,r)$ , and let $f_0\mathrel {:=}\mathrm {id}:(W,R,r)\to (W,R,r)$ be the identity map.

Then, we fix a countably infinite set X disjoint from W, and enumerate all tuples of

$$\begin{align*}(W\cup X)^2\cup \bigcup_{\Diamond ^mp\to \Diamond^n p\in \Phi }(W\cup X)^{2}\times \{\Diamond^mp\to \Diamond^np\}, \end{align*}$$

which is countable as $\Phi , W, X$ all are countable. $(W_{i+1}, R_{i+1}, r_{i+1})$ and $f_{i+1}$ are then constructed from $(W_{i}, R_{i}, r_i)$ and $f_{i}$ by applying the relevant preceding sublemma to the least tuple

$$\begin{align*}\overline{x}\in (W\cup X)^2\cup \bigcup_{\Diamond ^mp\to \Diamond^n p\in \Phi }(W\cup X)^{2}\times \{\Diamond^mp\to \Diamond^np\} \end{align*}$$

of our enumeration constituting a defect for $(W_{i}, R_{i}, r_i), f_i$ . (If there are no defects, set $(W_{i+1}, R_{i+1}, r_{i+1})\mathrel {:=}(W_{i}, R_{i}, r_i)$ and $f_{i+1}\mathrel {:=}f_i$ .)

There are two types of defects. First, a tuple of the form $\bar {x}=(x,y)\in (W\cup X)^2$ constitutes a defect for $(W_{i}, R_{i}, r_i), f_i$ if

$$\begin{align*}xR_iy\quad \text{yet there is no } y'\in W_i \text{ s.t. } xR_iy',\; \text{d}_i(y')=\text{d}_i(x)+1,\; f_i(y')=f_i(y), \end{align*}$$

and in this case Lemma 3.3 is applied.

Second, a tuple of the form $\bar {x}=(x,z, \Diamond ^mp\to \Diamond ^np)$ constitutes a defect for $(W_{i}, R_{i}, r_i), f_i$ if

$$ \begin{align*} xR_i^mz\quad &\text{yet there are no } w_1,\ldots, w_{n-1}\in W_i\\ &\text{s.t. } xR_iw_1R_i\cdots R_iw_{n-1}R_iz\text{ and }\text{d}_i(w_j)=\text{d}_i(x)+j, \end{align*} $$

and in this case Lemma 3.2 is applied.

The added points—namely, $\{u\}=W_{i+1}\setminus W_{i}$ when applying Lemma 3.3, and $\{u_1, \ldots , u_{n-1}\}=W_{i+1}\setminus W_{i}$ when applying Lemma 3.2—are drawn from $X\setminus W_i$ , which is possible as $X\setminus W_i$ is infinite for all $i\in \omega $ , since we only draw finitely many points in each application of a sublemma.

Letting

$$\begin{align*}W'\mathrel{:=}\bigcup_{i\in \omega} W_i, \quad R'\mathrel{:=}\bigcup_{i\in \omega} R_{i}, \quad r'\mathrel{:=} r, \quad f\mathrel{:=}\bigcup_{i\in\omega}f_i, \end{align*}$$

we have to show that

• • $f:(W', R')\to (W,R)$ is a p-morphism with $f(r')=r$ ;

• • $(W',R')$ is rooted at $r'$ and satisfies conditions (2) and (3).

That f is well-defined as a function follows from all $f_i$ being functions and that, by definition, $f_{i+1}{\upharpoonright } W_i=f_i$ ; and that $f(r')=r$ is a consequence of $r'=r$ and $f_0=\mathrm {id}$ . It satisfies the forth clause because each $f_i$ does, and, likewise, it satisfies the back clause because each $f_i$ does. Thus, we conclude that f is a p-morphism.

Next, that $(W',R')$ is rooted at $r'=r$ follows from each $(W_i, R_i)$ being rooted at $r_i=r$ .

Lastly, to see that it satisfies the conditions (2) and (3), first observe that for all $w\in W'=\bigcup _{i\in \omega } W_i$ , there is a least $i\in \omega $ s.t. $w\in W_i$ and, as highlighted in Remark 3.4, for all $j\geq i$ , $\text {d}_j(w)=\text {d}_i(w)$ ; hence $\text {d}'(w)=\text {d}_i(w)$ .

Now for condition (2), let $\Diamond ^mp\to \Diamond ^np\in \Phi $ be arbitrary and suppose $xR^{\prime ^m} z$ . Then there is a least $i\in \omega $ s.t. $\{x,z\}\subseteq W_i$ and $xR_i^mz$ . We also have $\text {d}'(x)=\text {d}_l(x)$ for all $l\geq i$ . If there are $w_1, \ldots , w_{n-1}\in W_i$ s.t. $xR_iw_1R_i\cdots R_iw_{n-1}R_iz$ and $\text {d}_i(w_j)=\text {d}_i(x)+j$ , then we have $xR'w_1R'\cdots R'w_{n-1}R'z\text { and }\text {d}'(w_j)=\text {d}'(x)+j$ , as required. If not, then as $(x,z)\in W_i^{2}\subseteq (W\cup X)^{2}$ , the tuple $(x,z,\Diamond ^mp\to \Diamond ^np)$ has been assigned some number $k\in \omega $ in our enumeration. So by construction, at some stage $l\leq i+k+1$ , Lemma 3.2 will have been applied to $(x,z,\Diamond ^mp\to \Diamond ^np)$ [or to another tuple whose resolution happens to fix this defect too],Footnote ⁴ and points $u_1,\cdots , u_{n-1}$ will have been added so that $xR_{l}u_1R_{l}\cdots R_{l}u_{n-1}R_{l}z\text { and }\text {d}_{l}(u_j)=\text {d}_{l}(x)+j$ . Consequently, also in this case, the condition holds, as then $xR'u_1R'\cdots R'u_{n-1}R'z$ and $\text {d}'(u_j)=\text {d}'(x)+j$ .

This shows that condition (2) holds. The proof of condition (3) is similar, but for completeness, we include it here as well. Accordingly, suppose $xR'y$ . Then there is a least $i\in \omega $ s.t. $\{x,y\}\subseteq W_i$ , and $\text {d}'(x)=\text {d}_l(x)$ for all $l\geq i$ . If there is $y'\in W_i$ s.t. $xR_iy', \text {d}_i(y')=\text {d}_i(x)+1,\text { and }f_i(y')=f_i(y)$ , then we have $xR'y', \text {d}'(y')=\text {d}'(x)+1,\text { and }f(y')=f(y)$ , as required. If not, then as $(x,y)\in W_i^{2}\subseteq (W\cup X)^{2}$ , the tuple has been assigned some number $k\in \omega $ in our enumeration. So by construction, at some stage $l\leq i+k+1$ , Lemma 3.3 will have been applied to $(x,y)$ , and a point u will have been added so that $xR_{l}u, \text {d}_{l}(u)=\text {d}_{l}(x)+1, \text { and }f_{l}(u)=f_{l}(y)$ . Consequently, also in this case, the condition holds, as then $xR'u, \text {d}'(u)=\text {d}'(x)+1, \text { and }f(u)=f(y)$ , which thereby completes the proof of the lemma.

Fact 3.6. Let $\mathfrak {M}=(W,R,V)$ and $\mathfrak {M}'=(W',R',V')$ be models, and $\mathbf {X}\subseteq \mathsf {Prop}$ a set of propositional variables. Then the following hold for all $k\in \omega $ :

• • If $w\sim ^{\mathbf {X}}_kw'$ , then for all formulas $\varphi $ such that $\mathsf {Prop}(\varphi )\subseteq \mathbf {X}$ and $\text {md}(\varphi )\leq k$ ,

  $$\begin{align*}\mathfrak{M},w\Vdash\varphi \qquad\text{iff}\qquad \mathfrak{M}', w'\Vdash \varphi. \end{align*}$$

• • ${\sim }\subseteq {\sim ^{\mathbf {X}}_{k+1}}\subseteq {\sim ^{\mathbf {X}}_k}$ .

• • If $\mathfrak {M}=\mathfrak {M}'$ , then $\sim ^{\mathbf {X}}_k$ is an equivalence relation on W.

• • If $\mathfrak {M}=\mathfrak {M}'$ and $\mathbf {X}$ is finite, then the set of $\sim ^{\mathbf {X}}_k$ -equivalence classes is finite.

Proof of the Filtration Lemma 2.7.

Suppose $\varphi $ is satisfied at a root $r\in W$ of a model $\mathfrak {M}=(W,R, V)$ satisfying (1) and (2) for each $\Diamond ^mp\to \Diamond ^np\in \Phi $ . Letting $\text {d}(x)\mathrel {:=}\text {d}_{r}(x)$ and $k\mathrel {:=}\text {md}(\varphi )$ , we extract a finite $\varphi $ -satisfying $\mathbf {K}\oplus \Phi $ model through a particular kind of filtration. First, we define a binary relation $\equiv $ on $W_{\leq k}\mathrel {:=}\{x\in W\mid \text {d}(x)\leq k\}$ as follows:

$$\begin{align*}x\equiv y \quad \text{iff} \quad \text{d}(x)=\text{d}(y) \text{ and } x\sim_{k-\text{d}(x)}y, \end{align*}$$

where we have suppressed the superscript $^{\mathsf {Prop}(\varphi )}$ and written $x\sim _{k-\text {d}(x)}y$ rather than $x\sim _{k-\text {d}(x)}^{\mathsf {Prop}(\varphi )}y$ .

Since $x\in W_{\leq k}$ means $\text {d}(x)\leq k$ , we have $k-\text {d}(x)\in \omega $ for all $x\in W_{\leq k}$ , so $\sim _{k-\text {d}(x)}$ is well-defined. One then easily checks that $\equiv $ is an equivalence relation on $W_{\leq k}$ using that the relations $\sim _{l}$ are equivalence relations (cf. Fact 3.6). Then, by the last bullet point of Fact 3.6 and the fact that the set of propositional variables occurring in $\varphi $ is finite, i.e., $|\mathsf {Prop}(\varphi )|<\aleph _0$ , we have that the set of $\equiv $ -equivalence classes

$$\begin{align*}W^f\mathrel{:=}\{|x| \mid x\in W_{\leq k}\} \end{align*}$$

is finite, where $|x|$ denotes the $\equiv $ -equivalence class of x.

We then define a relation $R^f\subseteq W^f\times W^f$ by setting $|x|R^f|y|$ iff $\text {d}(x)=k$ or

$$\begin{align*}\text{d}(x)<k,\quad \text{d}(y)\leq \text{d}(x)+1, \quad \text{and}\quad \exists y'(xRy'\text{ and } y'\sim_{k-\text{d}(x)-1}y). \end{align*}$$

Take note that we do not require that $y'\in |y|$ (and that $\text {d}(x)<k$ and $xRy'$ jointly imply $y'\in W_{\leq k}$ ).

Let us show that $R^f$ is well-defined, in that it doesn’t depend on the representatives of the equivalence classes. To see that it doesn’t depend on the representative for $|x|$ , observe that $x\equiv x'$ implies $\text {d}(x)=\text {d}(x')$ and $x\sim _{k-\text {d}(x)}x'$ , so if $xRy'$ and $y'\sim _{k-\text {d}(x)-1}y$ , then $x\sim _{k-\text {d}(x)}x'$ implies that there is $y"$ s.t. $x'Ry"$ and $y"\sim _{k-\text {d}(x)-1}y'$ , hence also $y"\sim _{k-\text {d}(x)-1}y$ . And to see that it doesn’t depend on the representative for $|y|$ , assume $y\equiv y"$ . Then $y\sim _{k-\text {d}(y)}y"$ , so $\text {d}(y)\leq \text {d}(x)+1$ implies $y\sim _{k-\text {d}(x)-1}y"$ (cf. Fact 3.6). Hence $y'\sim _{k-\text {d}(x)-1}y$ would imply $y'\sim _{k-\text {d}(x)-1}y"$ .

Thus, $(W^f, R^f)$ is a well-defined finite frame. To show that it is a $\mathbf {K}\oplus \Phi $ frame, we will use that the map $w\mapsto |w|$ is an R-homomorphism: if $xRy$ then $|x|R^f|y|$ , for all $x,y\in W_{\leq k}$ . Indeed, if $xRy$ , then clearly $\text {d}(y)\leq \text {d}(x)+1$ and $y\sim _{k-\text {d}(x)-1}y$ , so we have $|x|R^f|y|$ .

Now let $\Diamond ^mp\to \Diamond ^np\in \Phi $ be arbitrary and suppose $|x|R^f|y_1|R^f\cdots R^f |y_{m-1}| R^f|z|$ . We are to find $|w_1|,\ldots , |w_{n-1}|$ such that $|x|R^f|w_1|R^f\cdots R^f|w_{n-1}|R^f|z|$ . First, we observe that

$$\begin{align*}\text{d}(y_i)\leq \text{d}(x)+i\quad \text{and}\quad \text{d}(z)\leq \text{d}(x)+m, \end{align*}$$

since, whenever $|w|R^f|v|$ , we have $\text {d}(v)\leq \text {d}(w)+1$ : this is clear if $\text {d}(w)<k$ , and follows from $\text {d}(v)\leq k$ if $\text {d}(w)=k$ . Then, we continue by cases on $\text {d}(x)$ .

Case 1. If $\text {d}(x)\leq k-m$ , then we claim that there are $y_i'\in W$ , for $i\in \{1,\ldots , m\}$ , such that

$$\begin{align*}xRy_1'Ry_2'R\cdots Ry_m',\quad \text{d}(y_i')\leq \text{d}(x)+i, \quad y_i'\sim_{k-\text{d}(x)-i}y_i, \end{align*}$$

where we for convenience have denoted $y_m\mathrel {:=}z$ . We argue by induction on $i\in \{1,\ldots , m\}$ .

For the base case, since $|x|R^f|y_1|$ and $\text {d}(x)\leq k-m<k$ , there is $y_1'$ such that $xRy_1'$ and $y_1'\sim _{k-\text {d}(x)-1}y_1$ . The former implies $\text {d}(y_1')\leq \text {d}(x)+1$ .

For the inductive step, since $|y_j|R^f|y_{j+1}|$ and $\text {d}(y_j)\leq \text {d}(x)+j<k$ , we likewise find $y_{j+1}"$ such that $y_jRy_{j+1}"$ and $y_{j+1}"\sim _{k-\text {d}(y_j)-1}y_{j+1}$ . Since $\text {d}(y_j)\leq \text {d}(x)+j$ , Fact 3.6 gives us $y_{j+1}"\sim _{k-\text {d}(x)-j-1}y_{j+1}$ . Further, by the induction hypothesis, we have $y_j'\sim _{k-\text {d}(x)-j}y_j$ , so since $y_jRy_{j+1}"$ , there is $y_{j+1}'$ s.t. $y_j'Ry_{j+1}'$ and $y_{j+1}'\sim _{k-\text {d}(x)-j-1}y_{j+1}"$ . From the former we get

$$\begin{align*}\text{d}(y_{j+1}')\leq \text{d}(y_{j}')+1\overset{\text{IH}}{\leq}\text{d}(x)+j+1, \end{align*}$$

and from the latter we get $y_{j+1}'\sim _{k-\text {d}(x)-j-1}y_{j+1}$ , which completes the induction and establishes the claim.

By assumption, $(W,R)$ satisfies (2), so $xRy_1'Ry_2'R\cdots Ry_m'$ entails that there are $w_1, \ldots , w_{n-1}\in W$ s.t.

$$\begin{align*}xRw_1R\cdots Rw_{n-1}Ry_m'\quad \text{and}\quad \text{d}(w_{j})=\text{d}(x)+j. \end{align*}$$

Using this, we further split the case according to whether $\text {d}(x)\leq k-n$ .

Case 1a. If $\text {d}(x)> k-n$ , then there is $w_j$ with $\text {d}(w_j)=k$ for $1\leq j\leq n-1$ . So as $w\mapsto |w|$ is a homomorphism, we get a j-path $|x|R^f|w_1|R^f\cdots R^f|w_{j}|$ , and using that $|w_{j}|R^f|w_{j}|$ and $|w_{j}|R^f|z|$ as $\text {d}(w_j)=k$ , we can extend it to an n-path ending at $|z|$ .

Case 1b (Figure 1). If $\text {d}(x)\leq k-n$ , then

$$\begin{align*}\text{d}(w_{j})=\text{d}(x)+j\leq k-n+j<k, \end{align*}$$

so $w_j\in W_{\leq k}$ for all $j\leq n-1$ , hence

$$\begin{align*}|x|R^f|w_1|R^f\cdots R^f|w_{n-1}|. \end{align*}$$

Thus, it will suffice to show that $|w_{n-1}|R^f|z|$ . Since $\text {d}(w_{n-1})<k$ , we have to show that

$$\begin{align*}\text{d}(z)\leq \text{d}(w_{n-1})+1 \quad \text{and}\quad \exists z'(w_{n-1}Rz'\text{ and } z'\sim_{k-\text{d}(w_{n-1})-1}z). \end{align*}$$

The former holds because

$$\begin{align*}\text{d}(z)\leq \text{d}(x)+m\leq \text{d}(x)+n=\text{d}(w_{n-1})+1. \end{align*}$$

The latter is witnessed by $y_m'$ , in view of Fact 3.6 combined with

$$\begin{align*}y_m'\sim_{k-\text{d}(x)-m}y_m=z \qquad \text{and}\qquad \text{d}(x)+m\leq \text{d}(x)+n =\text{d}(w_{n-1})+1. \end{align*}$$

This completes the case where $\text {d}(x)\leq k-m$ .

Figure 1

Illustration of the key part of the argument, when $\text {d}(x)\leq k-n$ , for $m=2,n=3$ , so $|x|R^f|y_1|R^f|z|\Rightarrow \exists |w_1|, |w_2|:\; |x|R^f|w_1|R^f|w_2|R^f|z|$ .

Case 2. If $\text {d}(x)>k-m$ , then the subcase $\text {d}(x)=k$ is immediate, since in that case $|x|R^f|x|$ and $|x|R^f|z|$ . Accordingly, assume further that $\text {d}(x)<k$ , i.e., $\{0,\cdots , k-\text {d}(x)-1\}\neq \varnothing $ .

We denote $y_0\mathrel {:=}x$ and use that for all $i\in \{0,\ldots , k-\text {d}(x)-1\}$ , there is $y_{i+1}'$ s.t.

$$\begin{align*}y_iRy_{i+1}' \qquad \text{and} \qquad y_{i+1}'\sim_{k-\text{d}(x)-i-1}y_{i+1}. \end{align*}$$

This follows because $\text {d}(y_i)\leq \text {d}(x)+i$ and, for $i\leq k-\text {d}(x)-1$ , we have $\text {d}(x)+i\leq k-1<k$ . Thus, for such i, $|y_i|R^f|y_{i+1}|$ entails that there is $y_{i+1}'$ s.t. $y_iRy_{i+1}'$ and $y_{i+1}'\sim _{k-\text {d}(y_i)-1}y_{i+1}$ . And the latter implies $y_{i+1}'\sim _{k-\text {d}(x)-i-1}y_{i+1}$ , since $\text {d}(y_i)\leq \text {d}(x)+i$ .

Strengthening this, we claim that for all $i\in \{0,\ldots , k-\text {d}(x)-1\}$ , there is $y_{i+1}"$ s.t.

$$\begin{align*}xRy_1"Ry_2"R\cdots Ry_{k-\text{d}(x)}",\qquad \text{d}(y_{i+1}")= \text{d}(x)+i+1, \qquad y_{i+1}"\sim_{k-\text{d}(x)-i-1}y_{i+1}. \end{align*}$$

We prove this by induction on $i\in \{0,\ldots , k-\text {d}(x)-1\}$ .

For the base case, since $x=y_0Ry_1'$ , we get by condition (1) that there is $y_1"$ s.t. $xRy_1", \text {d}(y_1")=\text {d}(x)+1,$ and $y_1"\sim y_1'$ . Since $y_{1}'\sim _{k-\text {d}(x)-1}y_{1}$ , it follows that $y_1" \sim _{k-\text {d}(x)-1}y_1$ .

For the inductive case, since $y_iRy_{i+1}'$ and, by IH, $y_{i}"\sim _{k-\text {d}(x)-i}y_{i}$ , there is $y_{i+1}"'$ s.t. $y_{i}"Ry_{i+1}"'$ and $y_{i+1}"'\sim _{k-\text {d}(x)-i-1}y_{i+1}'$ . So by condition (1), there is $y_{i+1}"$ s.t.

$$\begin{align*}y_i"Ry_{i+1}", \qquad \text{d}(y_{i+1}")=\text{d}(y_i")+1\overset{\text{IH}}{=}\text{d}(x)+i+1,\qquad y_{i+1}"\sim y_{i+1}"'. \end{align*}$$

Thus, as

$$\begin{align*}y_{i+1}"'\sim_{k-\text{d}(x)-i-1}y_{i+1}'\sim_{k-\text{d}(x)-i-1}y_{i+1}, \end{align*}$$

we also have $y_{i+1}" \sim _{k-\text {d}(x)-i-1}y_{i+1}$ , as desired.

With the induction completed, it now follows that $|x|R^f|y_1"|R^f|y_2"|R^f\cdots R^f|y_{k-\text {d}(x)}"|$ , because $w\mapsto |w|$ is a homomorphism. This path can be extended to an n-path ending at $|z|$ , as we have $|y_{k-\text {d}(x)}"|R^f|y_{k-\text {d}(x)}"|$ and $|y_{k-\text {d}(x)}"|R^f|z|$ because $\text {d}(y_{k-\text {d}(x)}")=\text {d}(x)+k-\text {d}(x)=k$ .

This completes the case where $\text {d}(x)>k-m$ , and we may therefore conclude that $(W^f, R^f)$ is a $\mathbf {K}\oplus \Phi $ frame.

Finally, we let $\mathfrak {M}^f\mathrel {:=}(W^f,R^f,V^f)$ , where $V^f$ is the valuation on $(W^f, R^f)$ defined by setting

$$\begin{align*}V^f(p)\mathrel{:=}\{|x|\mid x\in V(p)\}, \end{align*}$$

for all $p\in \mathsf {Prop}(\varphi )$ . Note that this is well-defined. We proceed to show that for all $x\in W_{\leq k}$ and $\psi \in \mathrm{sub}(\varphi )$ with $\text {md}(\psi )\leq k-\text {d}(x)$ :

$$\begin{align*}\mathfrak{M},x\Vdash \psi\qquad \text{iff}\qquad \mathfrak{M}^f, |x|\Vdash \psi. \end{align*}$$

As $\mathfrak {M},r\Vdash \varphi , \text {d}(r)=0, \text {md}(\varphi )=k$ , and $\varphi \in \mathrm{sub}(\varphi )$ , this would imply $\mathfrak {M}^f, |r|\Vdash \varphi $ , thereby completing the proof.

We prove this claim by an induction on the modal depth of $\psi \in \mathrm{sub}(\varphi )$ . For the base case, we prove the claim holds for all $\psi \in \mathrm{sub}(\varphi )$ with $\text {md}(\psi )=0$ . Since we, by definition, have

$$\begin{align*}\mathfrak{M},x\Vdash p\qquad \text{iff}\qquad \mathfrak{M}^f, |x|\Vdash p \end{align*}$$

for all $x\in W_{\leq k}$ and all propositional variables $p\in \mathsf {Prop}(\varphi )$ , an easy induction establishes this biimplication for all Boolean combinations of propositional variables from $\mathsf {Prop}(\varphi )$ , hence for all formulas $\psi \in \mathrm{sub}(\varphi )$ with $\text {md}(\psi )=0$ .

For the inductive step, suppose for some $i\in \{0,\ldots , k-1\}$ that the claim holds for all $\psi \in \mathrm{sub}(\varphi )$ with $\text {md}(\psi )\leq i$ . We show it holds for all $\psi \in \mathrm{sub}(\varphi )$ with $\text {md}(\psi )=i+1$ . The proof is by structural induction on $\psi $ , where, once again, the Boolean cases are straightforward. So suppose $\psi =\Diamond \chi $ . Then $\text {md}(\psi )=i+1$ implies $\text {md}(\chi )=i$ ; and $\psi \in \mathrm{sub}(\varphi )$ implies $\chi \in \mathrm{sub}(\varphi )$ . Let $x\in W_{\leq k}$ with $\text {md}(\psi )\leq k-\text {d}(x)$ be arbitrary, and note that $\text {d}(x)\leq k-i-1$ .

If $\mathfrak {M},x\Vdash \Diamond \chi $ , there must be $y\in W$ such that $xRy$ and $\mathfrak {M},y\Vdash \chi $ . Since $xRy$ and $\text {d}(x)\leq k-i-1$ , we get that $\text {d}(y)\leq k-i$ , whence $\text {md}(\chi )=i\leq k-\text {d}(y)$ and $y\in W_{\leq k}$ . Hence we can apply the induction hypothesis, yielding

$$\begin{align*}\mathfrak{M}^f, |y|\Vdash \chi \end{align*}$$

and thus witnessing

$$\begin{align*}\mathfrak{M}^f, |x|\Vdash \Diamond\chi, \end{align*}$$

as $w\mapsto |w|$ is a homomorphism, so $xRy$ implies $|x|R^f|y|$ , for $x,y\in W_{\leq k}$ .

Conversely, if $\mathfrak {M}^f,|x|\Vdash \Diamond \chi $ , then there is $|y|$ such that $|x|R^f|y|$ and $\mathfrak {M}^f,|y|\Vdash \chi $ . Observe that since $\text {d}(x)\leq k-i-1$ , we have $\text {d}(x)<k$ , hence $|x|R^f|y|$ entails that $\text {d}(y)\leq \text {d}(x)+1$ and there is $y'\in W$ with $xRy'\text { and } y'\sim _{k-\text {d}(x)-1}y$ . So we have

$$\begin{align*}\text{md}(\chi)=i\leq k-\text{d}(x)-1\leq k-\text{d}(y), \end{align*}$$

hence by the induction hypothesis,

$$\begin{align*}\mathfrak{M}, y\Vdash \chi. \end{align*}$$

Lastly, because $y'\sim _{k-\text {d}(x)-1}y$ and $\text {md}(\chi )\leq k-\text {d}(x)-1$ , Fact 3.6 yields

$$\begin{align*}\mathfrak{M}, y'\Vdash \chi, \end{align*}$$

whence

$$\begin{align*}\mathfrak{M}, x\Vdash \Diamond\chi, \end{align*}$$

as required.