A relation between M₀ and W

The W-axiom looks quite different from the others. It is easily seen to follow semantically from both M and P. M has been weakened to M₀ and W is no longer derivable over M₀ as was seen in theorem 6.3. M₀ does however semantically imply something similar to W. The frame condition of M₀ excludes the possibility of descending (w.r.t. the R-relation) two worlds with an S_x-relation. This is reflected by a principle W₀, which can be seen as a weakening of the consequent of W.

$$W_0 : \ \ A\rhd B\rightarrow A\rhd B\wedge \Box \Box \neg A .$$

As M₀ is modally complete we must have $\mathit{ILM_0}\vdash W_0$. Indeed a pure syntactical proof exists. This proof can be extracted from the application of the construction method to this very case. So suppose $\mathit{ILM_0}\nvdash W_0$, and apply the construction method. We have to construct a model where some instantiation of W₀ does not hold. For that we first consider a maximal $\mathit{ILM_0}$-consistent set w₀containing $\neg (p\rhd q\rightarrow p\rhd q\wedge \Box \Box \neg p)$. Specifically $p\rhd q \in w_0$ and $\neg(p\rhd q \wedge \Box \Box \neg p)\in w_0$. So in w₀ we have the problem $\neg(p\rhd q \wedge \Box \Box \neg p)$. We solve this problem by introducing a $q\wedge \Box \Box \neg p$ critical successor w₁ of w₀, where p holds. See the figure below. Now we have a deficiency in w₀. So conform the construction method, we add w₂ where q holds.

This w₂ also lies $q\wedge \Box \Box \neg p$-critically above w₀, but as $q \in w_2$ we must have $w_2 \Vdash \Diamond \Diamond p$. So $\Diamond \Diamond p$ is a problem of w₁ (note that $\Diamond \Diamond p\leftrightarrow_{\mathit{IL}} \neg(\Diamond p\rhd \bot )$), and will be eliminated by adding an R-successor w₃ of w₂ such that $w_3\Vdash \Diamond p$. But also we have $w_3\Vdash \Box \neg \Diamond p$, i.e. $w_3\Vdash \Box \Box \neg p$. This was built into lemma 5.3. As $w_3\Vdash \Diamond p$ we must now introduce the R-successor w₄ of w₃ with $w_4\Vdash p$. So now we have a deficiency in w₀ w.r.t. w₄. This would be solved by introducing w₄, still in the $q\wedge \Box \Box \neg p$-cone of w₀, such that $w_4\Vdash q$. We have $w_3\subset_{\Box} w_5$, so $\Box \Box \neg p \in w_5$. But as $w_0 \prec_{\mbox{\footnotesize {$q\wedge \Box \Box \neg p$ }}} w_5$ and $w_5\Vdash q$, we should have $\neg \Box \Box \neg p \in w_5$. This can not be the case so indeed W₀ must hold. This argument can be captured in a purely syntactical proof.
Suppose $A\rhd B$. ( $A\rhd B\in w_2$.) Then one has $A\rhd (B\wedge \Box \Box \neg A)\vee (B\wedge \Diamond \Diamond A)$.(The last disjunct holds at w₂.) But $B\wedge \Diamond \Diamond A \rhd \Diamond A$.(We have $w_3\Vdash \Diamond A$.), so also $B\wedge \Diamond \Diamond A \rhd \Diamond A \wedge \Box \neg \Diamond A$. (This trick is incorporated in lemma 5.3.) Under the assumption of $A\rhd B$, by M₀ we have $\Diamond A \wedge \Box \Box \neg A \rhd B \wedge \Box \Box \neg A$. (This is the translation of $w_3\subset_{\Box} w_5$.) Using transitivity we obtain: $A\rhd B \rightarrow B\wedge \Diamond \Diamond A \rhd B \wedge \Box \Box \neg A$. So we can derive $A\rhd B \rightarrow A\rhd B\wedge \Box \Box \neg A$ in $\mathit{ILM_0}$.