There is a straightforward proof of the compactness theorem for propositional logic (see here) involving the following steps:
- Start with a finitely satisfiable set
- Extend the set into a set that includes every formula, or its negation
- Show that this extended set is finitely satisfiable
- Define a valuation V to make every proposition in the extended set true
- Take an arbitrary formula, with all of its atoms, from the original set; this set must be finitely satisfiable
- Show that any valuation satisfying the arbitrary formula + its atoms is equal to V.
Many modal logics are compact, but I have only seen a proof using First-Order Logic completeness + the Standard Translation, and another proof using the theory of ultraproducts. Why can the proof above not be adapted to modal logic?
Specifically - the definition of satisfiability is very similar in modal logic. It seems that we can simply adapt the proof to the modal version of "valuation" rather than the propositional version... at what point would this idea fail?
This similarity is superficial: there's a crucial way in which modal logic is closer to first-order logic in this respect. In propositional logic a model is basically the same thing as a complete theory: if $\Gamma$ is a maximal complete propositional theory, we just consider the valuation sending a propositional atom $a$ to $\top$ if $a\in\Gamma$ and $\perp$ if $\neg a\in\Gamma$, and check that this is in fact a "model" of $\Gamma$ in the sense of propositional logic.
By contrast, in modal and first-order logic it takes work to go from a complete theory to a model of that theory. Intuitively I'd say that the main point is that semantics in the sense of modal and first-order logic involves things which are not necessarily directly referred to in the language. In modal logic, these are the worlds. A model in the context of modal logic is a family of simple objects (= propositional models) connected to each other in a structured way (the underlying frame). The presence of this additional structure, which isn't explicitly determined by the language, makes the passage from complete theories to models nontrivial and resemble the first-order rather than propositional case.