I'm trying to construct an S5 proof of ⊢◻(◻P→◻Q)∨◻(◻Q→◻P).
I know that ϕ∨ψ is equivalent to ~ϕ→ψ, and so what I'm really trying to derive is ~◻(◻P→◻Q)→◻(◻Q→◻P) (which is equivalent to ◊~(◻P→◻Q)→◻(◻Q→◻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
as well as the rules modus ponens (ϕ, ϕ→ψ ⊢ψ) and necessitation (ϕ becomes ◻ϕ)).
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:
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→Q)→(~Q→~P) (true by propositional logic (it's just the contrapositive)), then applying necessitation and the first axiom gives (◻P→◻Q)→(◻~Q→◻~P), but I can't see any obvious way to proceed from here.
I could also start by saying that (◻P→◻Q)→(~◻Q→~◻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.