I am following the proof of:
Let $\tau$ be a modal similarity type containing only diamonds, and let $\phi$ be a $\tau$-formula. If $\phi$ is satisfiable, then it is satisfiable on a finite model.
I am just proving it for the basic modal language, that is, we only have one diamond $\diamond$
The proof is:
Fix a modal formula $\phi$ with $deg(\phi) = k$. We restrict our modal similarity type $\tau$ and our collection of proposition letters to the modal operators and proposition letters actually occurring in $\phi$. Let $M_1,w_1$ be such that $M_1,w_1\vdash \phi$ . By Proposition 2.15, there exists a tree-like model $M_2$ with root $w_2$ such that $M_2,w_2\vdash \phi$ . Let $M_3 := (M_2 \upharpoonright k)$. By Lemma 2.33 we have $M_2,w_2$ is $k$-bisimilar to $M_3 ,w_2$, and by Proposition 2.31 it follows that $M_3,w_2\vdash \phi$.
The construction of $M_4$ starts here.
By induction on $n \le k$ we define finite sets of states $S_0,...,S_k$ and a (final) model $M_4$ with domain $S_0\cup \cdots\cup S_k$; the points in each $S_n$ will have height $n$. Define $S_0$ to be the singleton $\{w_2\}$. Next, assume that $S_0,...,S_n$ have already been defined. Fix an element $v$ of $S_n$. By Proposition 2.29 there are only finitely many non-equivalent modal formulas whose degree is at most $k$, say $1,..., m$. For each such formula that is of the form $\diamond \phi$ and holds in $M_3$ at $v$, select a state $u$ from $M_3$ such that $Rvu$ and $M_3,u\vdash \phi$. Add all these us to $S_n+1$, and repeat this selection process for every state in $S_n$. $S_{n+1}$ is defined as the set of all points that have been selected in this way.
Finally, define $M_4$ as follows. Its domain is $S_0\cup\cdots S_k$; as each $S_i$ is finite, $M_4$ is finite. The relations and valuation are obtained by restricting the relations and valuation of M3 to the domain of M4. We can prove that $M_4,w_2$ is $k$-bisimilar to $M_3,w_2$.
The last sentence is actually left as an exercise which is not seems to be easy enough to solve within some hours. Could someone please tell me how to prove it (use some relative theorems?) or give some hint please?
The most important question is that: what is the relation defining an $k$-bisimulation here?
Thank you for any help.