Axiomatic proof of $\vdash_{S4} \square P\rightarrow\square\lozenge\square P$ in S4

Question

As the title explains, I'm trying to give an axiomatic proof of $\vdash_{S4} \square P\rightarrow\square\lozenge\square P$.

This is quite simple to prove in B, but I'm struggling to see how it's done in S4. I'd really appreciate any help you could offer.

In S4, I have the following axioms:

A1: $\phi\rightarrow (\psi \rightarrow \phi)$

A2: $(\phi \rightarrow (\psi \rightarrow \chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi \rightarrow\chi)) $

A3: $(\text{~}\psi \rightarrow \text{~}\phi)\rightarrow((\text{~}\psi \rightarrow \phi)\rightarrow\psi)$

K: $\square(\phi\rightarrow\psi)\rightarrow (\square\phi\rightarrow\square\psi)$

T: $\square\phi \rightarrow \phi$

S4: $\square\phi\rightarrow\square\square\phi$

and the rules necessitation (i.e. we can make $\phi$ into $\square\phi$ for any sentence $\phi$ and modus ponens.

Answer 1

From contrapositive of axiom T, $A\to\lozenge A,$ applying necessitation and taking $A=\square P$ gives $\square(\square P\to \lozenge\square P),$ which via K gives $\square\square P\to \square\lozenge\square P.$ Then axiom $\square P\to \square \square P$ finishes it off.