next up previous contents
Next: Problems Up: The modal completeness of Previous: Tools

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 m0 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:

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

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.



 
next up previous contents
Next: Problems Up: The modal completeness of Previous: Tools
Joost Joosten
2000-02-07