TASK: Given a set $\Gamma$ of propositional modal formulas where every finite subset of $\Gamma$ is satisfiable (say: $\Gamma$ is finitely satisfiable), show that $\Gamma$ itself is satisfiable.
IDEA: For propositional logic, a common proof is to build a set $\Omega$ of each superset $\Psi\supseteq\Gamma$, such that $\Psi$ is finitely satisfiable, and show that the partial order $(\Omega,\subseteq)$ contains a maximal element $\Phi_{max}\in\Omega$, which follows from Zorn's lemma, since every chain $C$ in $(\Omega,\subseteq)$ has an upper bound $\bigcup C$ in $(\Omega,\subseteq)$.
Then one can show that when exactly those propositions that hold true by a model $\mathfrak{I}$ are contained in $\Phi_{max}$, it follows that exactly all formulas that hold true by $\mathfrak{I}$ are contained in $\Phi_{max}$ (by structural induction). Consequently, $\mathfrak{I}$ is a model for $\Phi_{max}$, therefore it is a model for $\Gamma\subseteq\Phi_{max}$, thus $\Gamma$ is satisfiable.
ATTEMPT: I wonder how one can use this idea and extend it to a modal logic with multiple worlds, i.e. multiple interpretations $(\mathfrak{I}^w)_{w\in\mathfrak{W}}$ make a model. It is apparently not suffient to build $\Phi_{max}$ only once, as a formula $\Box\psi$ depends on all interpretations, but a set $\Gamma$ of modal formulas is satisfiable if and only if there is some world $w\in\mathfrak{W}$ such that $\Gamma$ is satisfiable in $w$. (So we cannot argue for $(\mathfrak{I}^w)_{w\in\mathfrak{W}},w\vDash\Box\psi$ iff $\Box\psi\in\Phi_{max}$, since required information is hidden from $\Phi_{max}$.)
My first idea was to consider sets in $ML\times\mathfrak{W}$, so for a maximal set it can be argued whether it contains $(\Box\psi,w)$, by testing if it contains $(\psi,w')$ for all $w'\in\mathfrak{W}$. But I fail to build such a maximal set $\Phi_{max}\subseteq ML\times\mathfrak{W}$ with the property of finite satisfiability containing supersets of the given $\Gamma\subseteq ML$.
Are you aware of a compactness proof for modal logics following this idea, or do you have an idea for a construction of $\Omega$ on which Zorn's lemma can be applied, such that a model for $\Phi_{max}$ can be constructed to imply satisfiability of $\Gamma$?
(I prefer this approach over using a standard translation, because the modal logic I consider is very hard to axiomatize in first-order logic (e.g. it requires all ZFC axioms to be part of a translation for a certain operator to state required set-theoretic properties). But it is only propositional and extends $S5$. Can it really be so hard to show compactness?)