Understanding a compactness proof for modal logics which uses a standard translation

Question

In the book Modal Logics (pp.$\,$84$-$85) of Patrick Blackburn, Maarten de Rijke and Yde Venema (alternatively, here,$\,$p.11$\,$"PROPOSITION $4$"), the authors claim that compactness for their basic modal logic can be proven by reducing it to the compactness theorem of first-order logic as explained in the following. (They did not provide the proof itself but only claim its existence.)

We can translate any formula in basic modal logic ($ML$) to first-order logic ($FOL$) using a standard translation $ST_x:ML\rightarrow FOL$ ($x$ being a first-order variable) with:

1. $ST_x(p_i)=P_i x$, for every proposition $p\in PROP$
2. $ST_x(\bot)=x\ne x$
3. $ST_x(\lnot\psi)=\lnot ST_x(\psi)$
4. $ST_x(\psi\lor\varphi)=ST_x(\psi)\lor ST_x(\varphi)$
5. $ST_x(\Box\psi)=\forall y(Rxy\rightarrow ST_y(\psi))$

Now, we can take every modal structure $\mathfrak{M}=(W,R,V)$ as first-order structure, since it provides the set of worlds $W$ as domain together with relations $R^\mathfrak{M}$, and $P_i^\mathfrak{M}:=V(p_i)$.
So we have a theorem:

For all modal structures $\mathfrak{M}$ it is $\mathfrak{M},w\vDash_{ML}\psi$ if and only if $\mathfrak{M}\vDash_{FOL}ST_x(\psi)[x\leftarrow w]$,
where $[x\leftarrow w]$ means that $w$ is assigned to the free FOL-variable $x$.

Now they claim (without proof) that:

we can use this bridge to import results, ideas, and proof techniques from one to the other

by which they include compactness. But in order to show the compactness theorem for $ML$, we have to show as a Lemma that every $ML$-formula $\psi$ is satisfiable if and only if $ST_x(\psi)$ is satisfiable. Clearly, we can show "$\Rightarrow$" by using the $\mathfrak{M}$ that satisfies $\psi$ to construct a satisfying structure for $ST_x(\psi)$ as explained. But how can we prove that if $ST_x(\psi)$ has a model (i.e. a satisfying FOL-structure), then $\psi$ has a model (i.e. a satisfying modal structure)? Or why would we not need to do this?

My idea would be to afterwards set up the compactness proof as follows.
Let $\Gamma\subseteq ML$ be a satisfiable set of basic modal logic formulas. This is by Lemma (TODO) equivalent to $\{ST_x(\psi)|\psi\in\Gamma\}$ being satisfiable, which means by the compactness theorem for first order logic, that every finite subset $\Phi\subseteq\{ST_x(\psi)|\psi\in\Gamma\}$ is satisfiable, which by Lemma (TODO) means that every finite $\Phi\subseteq\Gamma$ is satisfiable.

How can we either show "$\Leftarrow$" of Lemma (TODO), or avoid it being required? Why can't it be that there is some $FOL$-structure which satisfies $ST_x(\psi)$, from which we cannot construct a modal structure $\mathfrak{M}$ to satisfy $\psi$? Since clearly, $FOL$-structures are much more general than modal structures.

Answer 1

If I got your question right, Proposition 2.47 of the blue book (or, Proposition 3 of the handbook) establishes equivalence of a modal formula and its translation (in corresponding models). As for compactness, it is perfectly explained in Example 2.48 of the blue book. It goes roughly like this: if we have a set of modal formulae, and every subset of the set is satisfiable (i.e. has a model), then it follows, by Proposition 2.47, that all subsets of the standard translation of the initial set are satisfiable as well. Hence, by compactness theorem, the whole set is satisfiable, and we can translate its formulae back to formulae of modal logic.