Correctness.

It is quite clear that the model ${\cal M_1}$ is an $\mathit{ILM_0}$-model. To be an $\mathit{ILM_0}$-model, the frame induced by ${\cal M_1}$ must be an $\mathit{ILM_0}$-frame, i.e. it must be an $\mathit{IL}$-frame and it must satisfy the typical $\mathit{ILM_0}$ frame condition. The model ${\cal M_1}$ has already seen to be conversely well-founded w.r.t. the R-relation. Actually the well-foundedness is the only frame condition which is not expressible by a first order quantor rank four formula. (Of course it is not at all f.o. expressible.) So if one of the other frame conditions were not true, some witnesses could be found. Now suppose there were w,x,y and z which falsify one of the frame conditions. Then already for some n₀ one has $w,x,y,z \in {\cal M}_{n_0}$. But just as before, it is easy to see that every ${\cal M}_n$ defines an $\mathit{ILM_0}$-frame hence also ${\cal M}_{n_0}$. This conflicts the assertion that ${\cal M_1}$ would not be an $\mathit{ILM_0}$-model. So indeed ${\cal M_1}$ defines an $\mathit{ILM_0}$-frame.

Invariants 2, 3 and 6 are proved inductively together. It is shown they hold in every ${\cal M}_n$.

• It is trivial as usual that all the invariants hold in the basis model.

• Suppose a new world y is added by eliminating a problem in x by setting xR_e^By.
  • It is clear that $x \prec y$. If x'Ry then either x'Rx, x'=x or x' is incomparable to x. In the first case it is easy to see that $x' \prec y$. In the latter case it must be so that x'Rx''S_x0xfor some x',x'' and x₀. Note that this x₀ is uniquely defined. We can take x'' such that x was introduced to eliminate a deficiency in x₀ w.r.t. x'' while taking intermediate points into account. So $x' \subset_{\Box} x$. (Here we use the induction hypothesis for invariant 6.) But as xRy and thus $x \prec y$, also $x' \prec y$.

  • Invariant 3 is preserved while eliminating a problem, for the only new S relation that is added, is by the closure under the frame conditions: $x'Ry' \rightarrow x'Sy'$; but then clearly $x' \subset_{\Box} y'$.

  • Now consider invariant 6 after the new world y has been added to eliminate a problem in x. The only new and interesting case to consider will be if these worlds x and y are involved, for example when x₀Rx₁Ry for some x₀ and x₁. Close inspection of the situation results in concluding $x_1 \subset_{\Box} x$. If x₁Rxor x₁=x this is clear. If neither of these is true, it must be so that x'Rx₁Rx''S_x'x for some x'' and unique x'. x'' can be chosen such that x has been introduced in the model to resolve a deficiency in x' w.r.t. x''. This has been done by the procedure of making an S_x'^x''-block. So the intermediate world with the highest amount of $\Box$ formulas has been used in this procedure (Induction!). Consequently $x_1 \subset_{\Box} x$. Indeed x is the world maximal w.r.t. $\Box$ inclusion.

• Now suppose a new world y' is added by eliminating a deficiency in x w.r.t. some world y.
  • If for some world x₀, x₀Ry' is demanded, it can only be the case that x₀ R x. Clearly $x \prec y'$ and, by induction $x_0 \prec x$, so $x_0 \prec y'$.

  • Consider the case when xRx'RyS_xy' with x,y, and y' still standing for the same designated symbols. As y' was introduced by applying the procedure of making an S_x^y-block, we can be sure that the intermediate world x'' maximal w.r.t. $\Box$-inclusion has been used in applying this procedure (induction again), so that $x'' \subset_{\Box} y'$. Consequently $x' \subset y'$.

  • Invariant 6 is easily seen to be true. x₀ R y' can occur only when x₀ R x. So every ``R path'' ending up in y' must pass through x. Consequently x is maximal w.r.t. the $\Box$-inclusion in this particular case.

This concludes the proof that invariants 2, 3 and 6 hold in every ${\cal M}_n$. It is easy to see that invariants 2 and 3 extend to the infinite model. Recalling our earlier consideration of ``end extensions'', forces us to conclude that invariant 6 extends to the infinite model as well.

It is quite easy to see that invariant 4 holds in every ${\cal M}_n$. The basic model trivially satisfies 4. If some y is added to the model to eliminate a problem in x', either x' is in C_x^B or it is not. Only the latter case needs some argument. If $y \in C_x^B$ and $x \notin C_x^B$, there must be some $x_1,x_2 \in C^B_x$ and some x₀ R x such that x₀Rx₁Rx₂and x₂ S_x0x'. x₂ can be chosen so that x was introduced to eliminate a deficiency in x₀ w.r.t. x₂. Hence $x_1 \subset_{\Box} x'$. As $x_1 \subset_{\Box} x'$ and $x' \prec y$, one has $x \prec_{\mbox{\footnotesize {B}}} y$. (Recall that $x \prec_{\mbox{\footnotesize {B}}} x_1$.) The situation is very easy if a new world is added by eliminating a deficiency. Thus every ${\cal M}_n$ satisfies invariant 4. The notion of criticalness also extends to the infinite model. Analogously invariant 5 is seen to be true. (For example one could apply the same strategy as in the case of $\mathit{ILM}$.) The verification of the invariants concludes the completeness proof.