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
M0 and W is no longer derivable over M0 as was seen in theorem
6.3. M0 does however semantically imply something similar
to W. The frame condition of M0 excludes the possibility of
descending (w.r.t. the R-relation) two worlds with an
Sx-relation. This is reflected by a principle W0, which can be
seen as a weakening of the consequent of W.
This w2 also lies
-critically above w0,
but as
we must have
.
So
is a problem of w1 (note that
), and
will be eliminated by adding an R-successor w3 of w2 such that
.
But also we have
,
i.e.
.
This was built into lemma
5.3. As
we must now introduce the
R-successor w4 of w3 with
.
So now we have a
deficiency in w0 w.r.t. w4. This would be solved by introducing
w4, still in the
-cone of w0, such
that
.
We have
,
so
.
But as
and
,
we should have
.
This
can not be the case so indeed W0 must hold. This argument can be
captured in a purely syntactical proof.
Suppose .
(
.) Then one has
.(The last
disjunct holds at w2.) But
.(We have
.), so also
.
(This trick is incorporated in lemma 5.3.) Under the
assumption of
,
by M0 we have
.
(This is the translation of
.) Using transitivity we obtain:
.
So we can derive
in
.