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

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.

• Perhaps remind the reader what the axioms of S4 are? – Henning Makholm Jan 29 at 20:14
• @HenningMakholm I've updated the question to include them! – user639595 Jan 29 at 20:23
• Just for my information: what does ◊ mean/satisfy? – rrogers Feb 5 at 19:21
• @rrogers In classical modal logic, $\lozenge$ can be taken as an abbreviation for $\lnot\square\lnot.$ (In much the same sense that $\exists x$ can be taken as an abbreviation for $\lnot\forall x\lnot$ in classical first order logic.) The meaning of these things can’t be summarized in a comment; if you’re interested, consult a reference on modal logic. – spaceisdarkgreen Feb 18 at 16:54

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.