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{array}{cc} y S_x z \rightarrow ( \Box A \in y \rightarrow \Box A \in z ) & (*) \end{array}$$

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 R_e^B 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.

• ord(x)=0. This means x = m₀. It follows from the invariants that $y \in C_{m_0}^B$ for at most one B. Our task is to eliminate all deficiencies in m₀ w.r.t. y while preserving all invariants and in particular invariant 3. All deficiencies in x (in this case x=m₀) w.r.t. y are dealt with by the so-called process of making an S_x^y-block. It is described below how this proceeds precisely. The main idea of this process is to provide y with a whole net of S_x-successors insuring that no deficiencies exist in xw.r.t. y or w.r.t. any other element y' in the S_x^y-block. Formally speaking, the term S_x-successor is somewhat misleading, suggesting a successor relation. We will not worry too much about this formally wrong name. The whole block is created in such a way that it lies B-critically above x. By doing so, at least in this step, no old, already dealt with, problems will re-emerge. This is the general philosophy behind the process of making an S_x^y-block.

• ord(x)=n+1. We could eliminate all the deficiencies in x w.r.t. y by again making an S_x^y-block. This however could create new deficiencies of order n+1 in other worlds. For example if x' S x. The typical M frame condition demands the whole S_x^y-block to be above x'. If also ord(x')=n+1, we probably have loads of new deficiencies of order n+1 by eliminating some in x. The induction hypothesis does not apply to them. For this reason not only the deficiencies in x are eliminated at this stage, but at the same time the deficiencies of all the worlds x'Ry with ord(x')=n+1. We call the set of all these worlds N_x^y. The procedure now consists of three parts.
  

  Because of invariant 5 one has that ycan only be in some C_x'^B for at most one x' in N_x^y. We call this world x₀, and start by making an S_x0^y-block to resolve the deficiencies in x₀ w.r.t. y. By doing so we have eliminated all deficiencies in x₀ while conserving the B-criticality. So if x₀ R_e^B y, we make the whole S_x0^y-block lie B-critically above x₀. If no such x₀exists we just omit this part.
  

  For every $x' \in N_x^y$ we have to eliminate deficiencies if any, w.r.t. all elements of the Sx0y-block. The process of doing so is called the proces of making an SyN-block. This is discussed in more detail below. N is some set of worlds, wich in our case we take to be Nxy. So for each y' in the Sx0y-block, an SNx0yy'-block is made to eliminate all deficiencies in Nxy w.r.t. that world y'. Note that Nxy=Nx0y. If one leaves the B-critical cone of x0, this can only be done by an $S_{z \neq x_0}$-successor. So again the B-critical cones are respected. After having done all this there are no more deficiencies in Nxy w.r.t. the just created blocks.
  

  For $x' \neq x_0$ there might still be some deficiency w.r.t. ythough. These are dealt with by making an S^y_Nx'^y-block. All deficiencies in N_x^y are thus eliminated. By doing so only new deficiencies of lower order may have arisen, but the induction hypothesis takes care of them.