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.

  • $\begingroup$ Perhaps remind the reader what the axioms of S4 are? $\endgroup$ – Henning Makholm Jan 29 at 20:14
  • $\begingroup$ @HenningMakholm I've updated the question to include them! $\endgroup$ – user639595 Jan 29 at 20:23
  • $\begingroup$ Just for my information: what does ◊ mean/satisfy? $\endgroup$ – rrogers Feb 5 at 19:21
  • $\begingroup$ @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. $\endgroup$ – 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.