Is the $D$ modal logic necessarily serial?

Question

I'm wanting to show in $D$ that $\sim \square (\square p \wedge \square \sim p)$.

Here's my attempt:

(1) Show $\sim \square (\square p \wedge \square \sim p)$

(2) $ \square (\square p \wedge \square \sim p) \quad $assumption for indirect derivation with double negation

(3)$ \square [\sim (\square p \supset \Diamond p) ]\quad $ equivalent to line (3)

(4) $\square p \supset \Diamond p \quad$ Axiom D

(5) $\square(\square p \supset \Diamond p )\quad$ Necessity Inference rule applied to (4)

Now it would be nice if lines 3 and 5 were a contradiction but they aren't quite.

Given a frame $\langle W,R\rangle$ we say that it is $serial$ iff for every $w\in W$ there exists some $w'\in W$ such that $wRw'$; now it can be shown that the $D$ axiom must be valid on every serial frame. It would appear if the converse is true -- namely, that we require every logic system which has $D$ as an axiom to be serial -- then in fact the above would give a contradiction because the above proof is given from the perspective of some fixed world $w$. If 3 and 5 are true and this frame is serial then there exists $w'$ such that $wRw'$ with both $\sim (\square p \supset \Diamond p) $ and $ (\square p \supset \Diamond p) $ true at $w'$. $Cleary$, this would be a contradiction at $w'$ and hence for that entire frame. But is it asking to much that every system which adopts $D$ is necessarily serial?

Answer 1

Yes, please see the following:

http://planetmath.org/modallogicd

Answer 2

Remember that D is an axiom schema, so from ◻(◻P->◊P) one can derive ◊(◻P->◊P), which is equivalent to ~◻(◻P & ◻~P) given classical negation and the dual property for the box and the diamond.