General outline of the proof

By the same means by which the modal completeness of $\mathit{ILM}$was verified, we now obtain a new result: the modal completeness of $\mathit{ILM_0}$. Again a countermodel is built by successively eliminating problems and deficiencies. Since in this case we have not succeeded in proving the finite model property we will not strive for termination of the construction. In the new case we have to end up with an $\mathit{ILM_0}$-frame. Let us recall the $\mathit{M_0}$-axiom and its corresponding frame condition. M₀ is the axiom $A \rhd B \rightarrow \Diamond A \wedge \Box C \rhd B \wedge \Box C$ and its frame condition is:

$$v R w R x S_v y R z \rightarrow w R z$$

In order to obtain this property in our model consisting of copies of maximal $\mathit{ILM_0}$-consistent sets of modal sentences, it suffices to choose y such that $w \subset_{\Box} y$. It turns out to be possible to do so. Fix again an ${\mathcal A}$ such that $\mathit{ILM_0} \nvdash \mathcal{A}$. (Again this font is a little unusual in the modal setting, but we again want to have the A free to use in the course of this chapter.) The set of relevant formulas R is as before, the smallest set of formulas containing ${\mathcal A}$ and closed under taking subformulas and single negations. As ${\mathcal A}$ is not derivable in $\mathit{ILM_0}$there exists a maximal $\mathit{ILM_0}$-consistent set m₀containing $\neg \mathcal{A}$. A model $\mathcal{M}$ is built above this m₀ so that the truth lemma will hold for all relevant formulas, and thus $\mathcal{M} , m_0 \Vdash \neg \mathcal{A}$. We have to provide ourselves with some tools before we can start with the actual construction.