Making an S_N^y-block.

The procedure of ``making an S<sub>N</sub><sup>y</sup>-block'' is quite similar to that of ``making an S_x^y-block''. The main difference is that we are eliminating deficiencies here of a whole bunch of worlds at the same time. Another thing is that we are not too worried about criticalness. Of all the worlds in N, for at most one $x_0 \in N$, we have that $y \in C_{x_0}^B$ by invariant 5. The procedure of ``making an S<sub>N</sub><sup>y</sup>-block'' is meant to deal with all deficiencies in $N \setminus \{ x_0 \}$ w.r.t. y in such a way that no new deficiencies in N w.r.t. the S<sub>N</sub><sup>y</sup>-block occur. But where we do not take x<sub>0</sub> into account while eliminating the deficiencies in N w.r.t. y, we might need to take x<sub>0</sub> into account while eliminating the deficiencies in N w.r.t. the S<sub>N</sub><sup>y</sup>-block. Invariant 3 is not violated though, because it is not possible to enter the S<sub>N</sub><sup>y</sup>-block from y via an S<sub>x0</sub>-successor. Therefore if some worlds in S<sub>N</sub><sup>y</sup> lie above x<sub>0</sub> (and this is possible if we eliminate a deficiency in x with x<sub>0</sub>Sx), they will not be in the B-critical cone of x<sub>0</sub> and hence we will not need to worry about their B-criticality. Their successors however end up in the B-critical cone anyway via the $\mathit{ILM}$-condition ( $S\circ R\subseteq R$). But this is alright, since, if $x' \prec_{\mbox{\footnotesize {B}}} x \prec y'$ with $x \in N$ and y' in the S<sub>N</sub><sup>y</sup>-block we automatically have $x' \prec_{\mbox{\footnotesize {B}}} y'$. So at this stage of the construction we need not be concerned about the criticality w.r.t. lower order nodes. The procedure of ``making an S_N^y-block'' is now described in detail.

• Find x₀ such that $x_0 \in N$ and x₀R_e^By for some B. This x₀ is unique if it exists and will be fixed in the sequel.

• At the start the S_N^y-block is nothing but the empty set.

• Provide every x' in $N \setminus \{ x_0 \}$ for which there is some deficiency of x' with respect to y, with a y' that resolves that particular deficiency in a way that $y \subset_{\Box} y'$. This can be done seeing that $x \prec_{\bot} y$ and applying lemma 4.6 for a $\bot$-critical successor. Again y' is chosen to be maximal w.r.t. $\Box$-inclusion. Include this y' in the S_N^y-block and define moreover y S_x' y' .

• Close off under the $\mathit{ILM}$ frame conditions in a minimal way.

Repeat the following steps as long as deficiencies wherever in N with respect to some element of the S_N^x-block exist.

• Take a pair $x' \in N$ and y' in the S_N^y-block such that x' R y' and there exists some deficiency of x' w.r.t. y'. Say $C \rhd D$ is this deficiency and $C \in y'$. First look if there is some world y'' in the S_N^y-block such that $D \in y''$ and both x' R y'' and $\forall E ( \Box E \in y' \rightarrow \Box E \in y'' )$. If this is so, define y' S_x' y'' and the deficiency has disappeared. If it is not possible to find such a y'', it must be created and added to the S_N^y-block. (Note again that checking whether a relevant y'' exists already is only necessary for establishing the finite model property; if we are just after completeness we can skip this part.) Using lemma 4.8 and the stipulation that $x' \prec_{\bot} y'$ guarantees the existence of such an object. Again we define in this case y' S_x' y''.

• Close off under the $\mathit{ILM}$ frame conditions.

The same observations as before insure the termination of this procedure.