# S5 proof of $\square(\square P\rightarrow\square Q)\vee\square(\square Q\rightarrow\square P)$

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.

(in S5 I have the axioms

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

$$\square\phi \rightarrow \phi$$

$$\lozenge\square\phi\rightarrow\square\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.

• What have you tried? – Jishin Noben Jan 30 at 10:15
• @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. – j j jameson Jan 30 at 11:00
• Have you tried checking it in the semantics? That is, is it semantically valid? – ShyPerson Feb 1 at 23:03
• Answered here – Jishin Noben Feb 2 at 0:03