# Model-theoretic characterization of local modal correspondence

I've been reading van Benthem's dissertation (available on ILLC's website) on modal correspondence theory. In Section I.3, he develops a model-theoretic characterization of modal formulas having first-order correspondence. That is, a modal formula has first-order correspondence iff it is preserved under ultrapower. His proofs are mainly stated for global correspondence and he just states 3.7 Theorem on local correspondence saying "[it] may be proved by using the same methods".

Here's my thought: a (second-order translation of a) modal formula $\phi(x)$ locally corresponds to first-order $\alpha(x)$ iff $\mathrm{Mod}(\phi(c)) = \mathrm{Mod}(\alpha(c))$ in the frame language expanded with a new constant symbol $c$. If closure under ultrapower implies closure under ultraproduct (a consequence of an analogue of Goldblatt's lemma 3.1), as far as $\mathrm {Mod}(\phi(c))$ is concerned, then 3.7 Theorem holds.

The original Goldblatt's Lemma embeds an ultraproduct $\prod_i F_i/U$ of frames in the ultrapower of the disjoint union $\bigoplus_i F_i$ of frames. Taking a disjoint union makes sense because the original frame language is purely relational. However, since my new language contains a constant symbol, it is unclear how to adapt the original argument a la Goldblatt.

How can I prove 3.7 Theorem?

• I believe I figured this out and might write the solution down later. – Pteromys Aug 3 '15 at 9:01