The construction

The main body of the construction procedure for obtaining our required $\mathit{ILM_0}$-model is quite analogous to the case of $\mathit{ILM}$. One difference is that we now deal with copies of maximal $\mathit{ILM_0}$-consistent sets, and that we have to satisfy another frame condition. The nomenclature will thus be exactly the same. In the case of $\mathit{ILM_0}$ we will not have ``there are no deficiencies'' as an invariant. We start again with an $\mathit{ILM_0}$-consistent set m₀ containing $\neg \mathcal{A}$. If $\mathit{ILM_0} \nvdash \mathcal{A}$. Again the only entity that can be defined globally is the forcing relation $\Vdash$. We set $x \Vdash P \Leftrightarrow P \in x$, for the propositional variables. The body of the procedure will now be as follows:

• As a first approximation of the required model, set its domain to be $\{ m_0 \}$ and $R = S = \varnothing$.

begin
As long as problems or deficiencies still do exist in the model, enter this loop:

• If a problem does exist, then pick one of lowest order and eliminate this very problem. After having done so, close off under the frame conditions.

• If some deficiency exist somewhere, then fix an x and a y, such that deficiencies in x w.r.t. y do exist. Eliminate all these deficiencies and close off under the frame conditions.

end

We choose the way of eliminating problems, respectively deficiencies, cleverly so as to have some useful properties in the model. The useful properties that we need in our model are stated again as invariants as they hold at the beginning and at the end of each loop.

1.

The frame is an $\mathit{ILM_0}$-frame. 

2.

$x R y \rightarrow x \prec y$.  

3.

$xRx'RyS_xy' \rightarrow x' \subset_{\Box} y'$.  

4.

$y \in C_x^B \rightarrow x \prec_{\mbox{\footnotesize {B}}} y$.  

5.

  $B \neq B' \rightarrow C_x^B \cap C_x^{B'} = \varnothing .$

6.

  $x R y R z \rightarrow [ \exists \ y' \ x R y' R z \wedge \forall y'' (x R y'' R z \rightarrow y'' \subset_{\Box} y' )]$.

Again one should run through the whole construction checking that these are indeed invariants. Surely they hold at the beginning of the loop. So we have to make sure that after every execution of the loop all the invariants hold.