Compactness and the canonical model in modal logic

logicmodal-logicpropositional-calculus

For simplicity, consider the modal logic $\mathsf{K}$, i.e. propositional calculus extended by the scheme

$$\Box(\phi\rightarrow\psi)\rightarrow(\Box\phi\rightarrow\Box\psi)$$

and the necessitation rule: From $\vdash\phi$, infer $\vdash\Box\phi$. The classical approach to proving completeness for modal logics w.r.t. some class of models or frames is the canonical model construction.

Abstractly, we'd proceed as follows:

  1. Proving some fundamental properties of maximal consistent sets in $\mathsf{K}$.
  2. Proving that every consistent set can be extended to a maximal consistent set.
  3. Constructing the canonical model, having as worlds the maximal consistent sets of the language.
  4. Proving the truth lemma, i.e. that a formula is valid in the canonical model at a certain world if and only if it is contained in the corresponding maximal consistent set.

However, this approach can be used to prove strong completeness which in turn implies semantical compactness(provided the proof systems is compact). My problem is, that I don't quite see, where the construction of the canonical model would break down if I would have a non-compact semantical part.

Best Answer

I think that the construction would break down at the second step.

If a given logic is not compact, then there is a set $\Gamma$ every finite subset of which is satisfiable, but $\Gamma$ itself is not. Therefore, while proving Lindenbaum Lemma, we cannot be sure that the union of countably many consistent sets $\Gamma = \bigcup_{n=0}^\infty \Gamma_n$ is satisfiable.

Classic approaches to tackle this problem include using a finite fragment of a language via some kind of a closure (PDL, KL), or putting additional requirements on maximal consistent sets (e.g. that there is always a witness for a negation of a quantified formula of Quantified ML).