Axiomatic proof in S4 I'm trying to prove the following formula in S4.
$\Box \Diamond \Box \Diamond P \rightarrow \Box \Diamond P$
I have mp, nec, K,D,T,S4 as well as the derived rule $\Diamond \Diamond \phi \rightarrow \Diamond \phi$. I also am able to make obvious moves from propositional logic. i.e. going from $\phi \rightarrow \psi$ to $(\phi \land \sigma) \rightarrow \psi$ etc.
But I can't seem to figure this deduction out. Each time I end up with an extra $\Diamond$ or $\Box$.
 A: Let's first note that in system K, we have derived rules: if $\varphi \rightarrow \psi$ is a theorem, then (a) $\square \varphi\rightarrow \square \psi$ is a theorem, and (b) $\lozenge \varphi\rightarrow \lozenge \psi$ is a theorem. For (a), assume $\varphi\rightarrow \psi$ is a theorem. By necessitation, $\square(\varphi\rightarrow \psi)$. By $(K)$ and modus ponens, $\square \varphi\rightarrow \square \psi$. For (b), assume $\varphi\rightarrow \psi$ is a theorem. Then $\lnot \psi\rightarrow \lnot \varphi$ is a theorem. By (a), $\square \lnot \psi\rightarrow \square \lnot \varphi$. Taking the contrapositive again, $\lozenge \varphi\rightarrow \lozenge \psi$.
Ok, now for the proof. By $(T)$, $\square \lozenge P\rightarrow \lozenge P$. By (b), $\lozenge \square \lozenge P\rightarrow \lozenge\lozenge P$. By the derived rule $\lozenge\lozenge \varphi\rightarrow \lozenge \varphi$ you mentioned in your question, $\lozenge \square \lozenge P\rightarrow\lozenge P$. By (a), $\square\lozenge \square \lozenge P\rightarrow\square\lozenge P$, as desired.
Note that the proof used modus ponens, necessitation, $(K)$, $(T)$, and $(4)$ in the form of the derived rule from your question. The proof did not use $(D)$, and indeed $(D)$ is usually not taken as an axiom in S4 modal logic.
