Correctness and termination

Troughout the whole contruction invariants played an important role. It has not yet been really proved that they indeed are invariants. As the construction method is inductively defined, we will prove the invariants by induction on the construction of the model. So, proving the correctness of an invariant consists of showing that it holds at the basis, i.e. the model $\langle \{ m_0\} , \varnothing , \varnothing , \Vdash \rangle$, and show that it is preserved in the inductive steps. Two inductive steps will be considered: eliminating a problem and eliminating a deficiency. Eliminating a deficiency in itself is an inductive process but it will not be necessary to consider it in total detail while proving the correctness of an invariant.

The proofs of the correctness of the invariants are quite laborious and do not involve any profound mathematics. We add them though, in order to provide a complete proof. The already convinced reader can just skip this part or skim it over.

The first invariant we met was $(*) : x S y \rightarrow x \subset_{\Box} y$. To prove this invariant we take the conjunction of this statement with invariant 2: $x R y \rightarrow x \prec y$. The inductive proof of this conjunction will run as follows.

• In the basis model there are no R or S relations, so both conjuncts are automatically satisfied.

• Suppose a new y is defined when eliminating a problem, say x R_e^B y, and the model is closed under the frame conditions in a minimal way. Note that $x \subsetneqq_{\Box} y$ and $\Box \neg B \in y \setminus x$. If the frame conditions demand x' S y, this can only be because the frame conditions impose x' R y because of for example x' S x. But in this case the induction hypothesis tells us $x' \subset_{\Box} x$, and as $x \subsetneqq_{\Box} y$, it is clear that $x' \subset_{\Box} y$. So $x' S y \rightarrow x' \subset_{\Box} y$ is thereby established. As $x' \subset_{\Box} x$ and $x \prec y$, we have $\Box A \in x \rightarrow A, \Box A \in y$. In other words we have $x \prec y$ as well as $x' \prec y$.

• Suppose now that a new world y' is created while eliminating a deficiency in x w.r.t. y. The world is chosen so that (*) holds. As y S_x y', one is obliged to define x R y'. But as y' is chosen by lemma 4.8 one has $x \prec y'$. It is easy to see that if x' R y' is imposed by the frame conditions then either x' S x or x' R x $(x' \neq x)$. If x' R x then $x' \prec x$ and by the transitivity of $\prec$, $x' \prec y'$. If x' S x then $x' \subset_{\Box} x$ and because of $x \prec y'$ one has $\Box A \in x' \Rightarrow \Box A \in x \Rightarrow A , \Box A \in y'$. Also there is a $\Box A \in y' \setminus x'$. So indeed $x' \prec y'$.

Invariant 1 is evidently seen to be true as all the time the finite construction is closed off under the frame conditions. And the frame conditions together with the construction method form a consistent process, i.e. never will one frame condition exclude the other.

Now we come to prove the fact that a B-critical cone of x lies indeed B-critically above x. For this is what invariant 3 actually says: $y \in C_x^B \rightarrow x \prec_{\mbox{\footnotesize {B}}} y$.

• Again the basis step is trivially fulfilled.

• Now consider the case that the frame conditions demand $y \in C_x^B$for some x and B: y here is the newly defined world, which was introduced to eliminate a problem in x', i.e. for some B', x' R_e^B' y. Of course we may assume that $x\neq x'$, otherwise things are trivial. We distinguish two different situations:

  • $x' \in C_x^B$. This implies $x \prec_{\mbox{\footnotesize {B}}} x'$ and combined with $x' \prec y$ this yields $x \prec_{\mbox{\footnotesize {B}}} y$.

  • $x' \notin C_x^B$. That the frame conditions impose $y \in C_x^B$, must be because x'' S x' for some $x'' \in C_x^B$. Hence we have $x'' \subset_{\Box} x'$. If now $A \rhd B \in x$ then $\neg A , \Box \neg A \in x''$ and so $\Box \neg A \in x'$ (because of x'' S x') and thus $\neg A , \Box \neg A \in y \ ( x' \prec y )$. Thus $x \prec_{\mbox{\footnotesize {B}}} y$. (It is also possible that x = x' and B =B' so that one trivially obtains $x \prec_{\mbox{\footnotesize {B}}} y$.)

• Suppose now y is introduced while eliminating a deficiency, and $y \in C_x^B$. We again distinguish two situations:

  • $\exists x' \in C_x^B \ x' R y$. Then the induction hypothesis applies to x' so $x \prec_{\mbox{\footnotesize {B}}} x'$. But because $x' \prec y$, the required $x \prec_{\mbox{\footnotesize {B}}} y$ is herewith confirmed.

  • $\neg ( \exists x' \in C_x^B \ x' R y )$. In this situation one must have y₀ S_x y for some $y_0 \in C_x^B$. By scrutinizing the process by which a deficiency is eliminated one must conclude that at some stage y has been added to the model by applying lemma 4.8 in making an S_x^y'-block. This means that y indeed lies B-critically above x.

Instead of proving invariant 4: $B \neq B' \rightarrow C_x^B \cap C_x^{B'} = \varnothing$, we will prove something stronger. First we define a new set ${\tilde{C}}_x^B$, of successors of x. We take ${\tilde{C}}_x^B$ the smallest set such that: $x R_e^B y \rightarrow y \in {\tilde{C}}_x^B$ and $y \in {\tilde{C}}_x^B \wedge y S y' \rightarrow y' \in {\tilde{C}}_x^B$. It is quite easy to show with induction on this definition that the invariant actually holds for ${\tilde{C}}_x^B$. That is $B \neq B' \rightarrow {\tilde{C}}_x^B \cap {\tilde{C}}_x^{B'} = \varnothing$.

• The basis model again is trivial.

• Suppose that y is added to the model while eliminating a problem in x' and the frame conditions force y to be in ${\tilde{C}}_x^B$. If $x\neq x'$ this can only be the case if for some $x'' \in \tilde{C}_x^B$ one has x'' S x' and x'' R y is thus forced. This also implies that $x' \in \tilde{C}_x^B$. By the same means one concludes $x' \in \tilde{C}_x^{B'}$ if $y \in \tilde{C}_x^{B'}$. The induction hypothesis then gives B = B'. If x = x' and the frame conditions impose $y \in \tilde{C}_x^B$ then this can only be because of x R_e^B y. It is clear then that y can't be in $\tilde{C}^{B'}_x$ for $B' \neq B$.

• Consider a new world y' which is added to eliminate a deficiency in x'w.r.t. y and suppose that the frame conditions demand $y'\in \tilde{C}^B_x$. Close inspection of the process of eliminating a deficiency yields the conclusion that y already must have been in $\tilde{C}^B_x$. The induction hypothesis tells us that ycan not be in $\tilde{C}^{B'}_x$ for another B'. So the same holds for y'.

Instead of invariant 5: $ord(x) = ord(y) \wedge x \neq y \rightarrow C_x^B \cap C_y^{B'} = \varnothing$we will prove the stronger invariant obtained by replacing C_x^B by ${\tilde{C}}_x^B$ in 5.

• The invariant is obviously satisfied in the basic model.

• Suppose that y is introduced to eliminate a problem in x'' and suppose moreover that the frame conditions demand $y \in \tilde{C}_x^B$. If $x'' \in \tilde{C}_x^B$ then the induction hypothesis tells us that $x'' \notin \tilde{C}_{x'}^{B'}$ for any $x' \neq x$ and ord(x') = ord(x). So the same holds for y. If $x'' \notin \tilde{C}_x^B$ and yet $y \in \tilde{C}_x^B$ is obligatory, it must be that x'' = x and x R_e^B y. ord(x') = ord(x)implies $x \notin \tilde{C}_{x'}^{B'}$ for any B'. So $y \in \tilde{C}_{x'}^{B'}$ for $x\neq x'$ is not possible.

• The case when a deficiency is introduced is completely analogous to the previously treated invariant 4.