I'm trying to construct an S5 proof of $\vdash\square(\square P\rightarrow\square Q)\vee\square(\square Q\rightarrow\square P)$.

I know that $\phi\vee\psi$ is equivalent to $\text{~}\phi\rightarrow\psi$, and so what I'm really trying to derive is $\text{~}\square(\square P\rightarrow\square Q) \rightarrow\square(\square Q\rightarrow\square P)$ (which is equivalent to $\lozenge\text{~}(\square P\rightarrow\square Q) \rightarrow\square(\square Q\rightarrow\square P)$), but I'm not sure what steps I'd have to take to reach this.

Your help would be appreciated.

(in S5 I have the axioms

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

$\square\phi \rightarrow \phi$


as well as the rules modus ponens ($\phi$, $\phi\rightarrow\psi$ $\vdash \psi$) and necessitation ($\phi$ becomes $\square\phi$)).

EDIT: here are the approaches that I've considered so far:

As above, I know that what I need to prove is of the form:

$\lozenge\text{~}(\square P\rightarrow\square Q) \rightarrow\square(\square Q\rightarrow\square P)$

I've tried working back from this to get to something more familiar that I would know how to prove, but without much success.

Taking the contrapositive certainly doesn't work because you just end up with the same thing but with Q and P swapped.

I could start by taking $(P\rightarrow Q) \rightarrow(\text{~}Q\rightarrow \text{~}P)$ (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives $(\square P\rightarrow\square Q) \rightarrow(\square \text{~}Q\rightarrow\square \text{~}P)$, but I can't see any obvious way to proceed from here.

I could also start by saying that $(\square P\rightarrow\square Q) \rightarrow(\text{~}\square Q\rightarrow\text{~}\square P)$, but again I see no obvious way to proceed because the negations make things more difficult.

I'm really at a loss as to how to actually approach this, so even just helping tell me how I get started would help a lot.

  • $\begingroup$ What have you tried? $\endgroup$ – Jishin Noben Jan 30 at 10:15
  • $\begingroup$ @JishinNoben I've edited to include what I've considered, but it's not much because I haven't been able to get very far at all. $\endgroup$ – j j jameson Jan 30 at 11:00
  • $\begingroup$ Have you tried checking it in the semantics? That is, is it semantically valid? $\endgroup$ – ShyPerson Feb 1 at 23:03
  • $\begingroup$ Answered here $\endgroup$ – Jishin Noben Feb 2 at 0:03

Your Answer

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

Browse other questions tagged or ask your own question.