The actual construction.

All the above ingredients make sure that the logic is complete. However there is no ingredient that would yield the finiteness of the model. In proving the completeness of $\mathit{ILM_0}$ an infinite model is thus provided as the limit of an iterative process. In the limit neither problems nor deficiencies should be present. Most likely, eliminating a problem or a deficiency will create many new problems and deficiencies as a side effect. It should be made sure that every problem or deficiency is at some stage eliminated. This can be done by adequate labeling as is also done in [MVar]. By means of a set I, the set of imperfections we will keep track of all the problems and deficiencies which have not yet been eliminated. The model construction can thus be represented by the following procedure.

• The first approach to the model will be to take the domain $\{ m_0 \}$and $R = S = \varnothing$. All the problems of m₀ are stored in I.

As long as I is nonempty repeat the following actions.

• Select the oldest member of I. If this is not uniquely defined, just pick arbitrarily one of the oldest. Old refers of course to how many repetitions the element has already been in I.
  • If this oldest member of I is a problem $\neg ( A \rhd B )$ in some world x, eliminate it by defining xR_e^By for an adequate y. This y is provided by lemma 5.2 and as usual is chosen such that $x \prec_{\mbox{\footnotesize {B}}} y$ and $A \in y$.
  • If the oldest member of I is a deficiency in some world x w.r.t. some world y, then eliminate it by making an S_x^y-block.
• Close off under the $\mathit{ILM_0}$ frame conditions in a minimal way. Add the new freshly born problems and deficiencies to I.

This construction method produces a whole series of $\mathit{ILM_0}$-models ${\cal M}_{0} \subset {\cal M}_{1} \subset {\cal M}_{3} \subset \ldots$. With each execution of the repeat loop the previous model is extended. In general, for no $n\in \omega$, ${\cal M}_{n}={\cal M}_{n+1}$ will hold. But one can consider ${\cal M_1} := \bigcup_{i \in \omega} {\cal M}_i$. It is clear that in ${\cal M_1}$ neither problems nor deficiencies hold. This of course under the assumption that all the invariants we used throughout the construction are indeed invariants, and also hold for the infinite model. If this is true, then problems that have been eliminated will never re-emerge. This is reflected by invariant 4. The main strategy for proving the invariants will be to prove their correctness for all ${\cal M}_n$, and then show that this extends to the infinite model. Before doing so it is useful to note some features of the chain of models ${\cal M}_{0} \subset {\cal M}_{1} \subset {\cal M}_{3} \subset \ldots$. First of all one can say there is a uniform upper bound to the height of the model. (The height is defined as the maximal length of some chain $x_0Rx_1R \ldots Rx_n$ in the model.) Therefore ${\cal M_1}$also has finite height. Thus ${\cal M_1}$ is conversely well-founded when it comes to the R-relation. Second and also important, one can see that ${\cal M}_{n+1}$ is sort of an ``end extension'' of ${\cal M}_n$ in the sense that no intermediate worlds will be added. So, if $xTy \in {\cal M}_n$ and $z \in {\cal M}_{n+1} \setminus {\cal M}_n$, then for no z, xTzTy for both T=S_xi as well as for T=R. Further it is clear that all defined notions like $R,\ S,\ C_x^B$, etc. are weakly monotonic increasing entities.