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?