next up previous contents
Next: The details of constructing Up: The construction Previous: Problems

Deficiencies

Deficiencies are harder to deal with and they demand an inductive treatment. Eliminating a problem was done by just defining some R successor. In this part we need to define the S transitions. They will be defined in such a way that one always has

\begin{displaymath}\begin{array}{cc}
y S_x z \rightarrow ( \Box A \in y \rightarrow \Box A \in z ) & (*)
\end{array}\end{displaymath}

By doing so, the special M frame condition can readily be incorporated. Actually (*) should properly be verified. One way of doing so is by means of invariants. The construction can roughly be seen as an initialization followed by a loop. An invariant is a property which holds after the initialization and after every execution of the loop. One of the invariants has already been encountered: ``there are no deficiencies''. Other useful invariants are:

1.
 The model is a finite $\mathit{ILM}$-model.

2.
  $xRy \Rightarrow x \prec y .$

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

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

5.
  $ ord(x) = ord(y) \wedge x \neq y \rightarrow C_x^B \cap C_y^{B'} =
\varnothing. $

All these properties can easily be checked while going through the construction. It should be made clear that these invariants hold at the beginning and after every execution of the loop.

The problem $\neg ( A \rhd B ) $ in m was taken care of by defining a B-critical successor m' to be its ReB successor. The thus obtained extension is closed off under the frame conditions of $\mathit{ILM}$ in a minimal way. By this we mean that the new S is taken to be the reflexive transitive closure of the previous one plus $\langle m,m'\rangle$, and the new R is taken to be the transitive closure of $\mbox{\lq\lq new $S$ ''}\circ R$. This again yields an $\mathit{ILM}$-frame.
If there are deficiencies in m with respect to m' we will prove by induction on ord(m) that all these deficiencies can be eliminated. More generally we prove by induction on ord(x) that all deficiencies in x w.r.t. y can be eliminated without new deficiencies occurring.


next up previous contents
Next: The details of constructing Up: The construction Previous: Problems
Joost Joosten
2000-02-07