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


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.


1 Answer 1


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).

  • $\begingroup$ I have read this before, however the version of the Lindenbaum Lemma I have seen only requires the union to be consistent, a property which we have immediately, if the proof system is compact. Also the canonical model then works only with consistency and not with semantic concepts. So, up to that point, even if the union is not satisfiable I see no problem as to why the proofs could not be carried out. However, the connection to the semantic concepts is then established in the Truth Lemma. Thus, I think the proof should rather break down there. Do you have any thoughts to this? $\endgroup$
    – blub
    Commented Mar 4, 2019 at 17:16
  • $\begingroup$ What does it mean for a proof system to compact? $\endgroup$ Commented Mar 4, 2019 at 17:37
  • $\begingroup$ I just mean that if $\Gamma\vdash\phi$ for some proof relation $\phi$, then already $\Gamma_0\vdash\phi$ for some finite subset $\Gamma_0\subseteq\Gamma$. Thinking of classical finitistic calculi, you get this property just by assuming that proofs are finite(which I did not specify directly). $\endgroup$
    – blub
    Commented Mar 4, 2019 at 18:10
  • $\begingroup$ Well, I think that you have already partially answered your question by mentioning the assumption that proofs are finite. For, if we consider infinitary rules of inference (rules with an infinite number of premises), then we should have additional requirements on $\Gamma$ (like the existence of a witness). $\endgroup$ Commented Mar 4, 2019 at 18:27
  • 1
    $\begingroup$ Exactly, those are the desirable proof-theoretic properties in this approach. The system in the back of my head while asking this question was finitary to begin with and I really wanted to focus on the point where semantical non-compactness stops the canonical model approach from working. I was just unsure about whether there is a precise point in the proof implicitly needing semantical compactness or if the truth lemma in general fails and it is more a case-by-case situation of why exactly. From the discussion with you and further investigations by myself, I take away the second. $\endgroup$
    – blub
    Commented Mar 4, 2019 at 18:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .