The construction

We have now provided ourselves with enough tools to start with the actual construction. Our construction material will consist of copies of elements of the earlier defined set $\widetilde{M}$. Step by step we will paste them together by means of defining the R and the S relation. So, again consider an ${\mathcal A}$ for which we have $\mathit{ILM}\nvdash \mathcal{A}$. Since ${\mathcal A}$ is not provable in $\mathit{ILM}$, there exists an m₀ in $\widetilde{M}$ containing $\neg \mathcal{A}$. This m₀ will be the starting point of the construction.
In order to be able to talk about the model under construction it is convenient to first introduce some ad hoc nomenclature.

Definition 4.9   For any world x of the model we define the order of this world to be the number of boxed formulas in $x \cap \mathit{BR}(\mathcal{A})$ minus the number of boxed formulas in $m_0 \cap \mathit{BR}(\mathcal{A})$. A boxed formula is a formula of the form $\Box A$.

Definition 4.10   A problem in x is a relevant sentence $\neg ( A \rhd B ) \in x$ such that there is no y with x R_e^B y and $A \in y$. The R_e^Brelation is just a special case of the R relation and will be introduced and treated later on. When we talk of the order of some problem we mean the order of the world in which the problem ``lives''.

Definition 4.11   A deficiency in x w.r.t. y is a relevant sentence $C \rhd D \in x$such that $C \in y$ and x R y but there is no y' with y S_x y' and $D \in y$.

Definition 4.12   For any world x in the model we define C_x^B, the B-critical cone of x, to be the smallest set of worlds such that $x R_e^B y \rightarrow y \in C_x^B$ and $y \in C_x^B \wedge y S_x y' \rightarrow y' \in C_x^B$.

The model will be built up in stages. At every stage an $\mathit{ILM}$-model is made out of the $\mathit{ILM}$-model of the previous stage. Eventually a model is obtained in which the desired truth lemma will hold. For example the R relation is not defined all at once but will be expanded as the construction proceeds. The only entity that will be globally defined is the $\Vdash$ relation. It will be defined as in all modal completeness proofs: $x \Vdash P$ iff $P\in x$ for propositional variables P. (Of course, we somewhat sloppily write $A\in x$ if A belongs to $\tilde{m}$ of which x is a copy.) The construction method can schematically be represented by the following:

• The first approach to our final model will be to set $M = \{ m_0 \}$, $R = \varnothing$ and $S = \varnothing$. Then enter the following loop:

begin
As long as problems still exist in the model, execute the following two steps:

• Locate a problem of minimal order and eliminate it. This should be done in such a way that no new problems of the same or lower order will be created. Close off under the $\mathit{ILM}$ frame conditions in a minimal way. (In order to have the $\mathit{ILM}$ frame condition, $R \subset S$, transitivity of both R and S, etcetera.)

• By having eliminated one problem, probably loads of deficiencies have emerged as a side-effect. Eliminate all these deficiencies. Again the resolving of these deficiencies should not create new problems of the same or lower order.

end

If termination of this process can be established then it is clear that the truth lemma holds. For the only part of the truth lemma which involves $\rhd$and hence the only part of the truth lemma that needs a proof could be formulated as ``there are no problems nor deficiencies''. After the initialization of the procedure, no deficiencies exist because in the model with just one node and no relations also $\Box \bot$ holds. At the end of each loop no deficiencies exist either. So if the process terminates there will be no more deficiencies. But if the process terminates this means that all problems have been eliminated. Now if the truth lemma holds, the observation that $\neg \mathcal{A} \in m_0$ concludes the completeness proof.
So it remains to show that both problems and deficiencies can be eliminated in such a way that termination is guaranteed.