Problems

Easiest to deal with are the problems. Say that $\neg ( A \rhd B )$is a problem for some world m. To eliminate this problem is to provide this m with an R-successor m' where A holds, in such a way that from m' it is impossible to reach some world where Bholds via an S_m-transition. As B should not hold in m' nor at any possible R-successor of m', we should take m' to lie B critically above m. We also must take care that starting in m'with an S_m-transition, it will never be possible to reach a world where B holds. We should so to say ``fence the S_m-scope of m'in''. This fencing in is performed by the so-called B-critical cone of m. We write C_m^B. So the whole B-critical cone of mwill lie B-critically above m, and the definition will insure that it will not be possible to leave the B-critical cone of m with an Ror an S_m transition. By doing so, we are sure that this particular problem $\neg ( A \rhd B ) \in m$ will never re-emerge.

The existence of a B-critical successor of m containing A is guaranteed by lemma 4.6. In our construction we thus define this entity m' to be an R_e successor of m. We write R_e instead of R because we want to be able to distinguish essential R relations which are added to eliminate a problem, from non-essential R relations (we write R_n) which are added either to restore the $\mathit{ILM}$ frame conditions or to eliminate deficiencies. By R we mean the transitive closure of $R_e \cup R_n$. Sometimes we write R_e^B to indicate that the added R_e transition is an intended B-critical one. It will turn out to be useful to have the maximality w.r.t. $\Box$-inclusion of m'. By this the finiteness of the construction can be guaranteed. All the R-successors of this m' will automatically be B-critical successors of m. It is therefore sufficient to ensure that by an S_m-transition it is impossible to leave the B-critical cone of m. This is incorporated in the construction and expressed by incariant 3 below.