S5 proof of ⊢◻(◻P→◻Q)∨◻(◻Q→◻P)

Question

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:

◊~(◻P→◻Q)→◻(◻Q→◻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→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.

Answer 1

Finding proofs in axiomatic proof systems is an unpleasant task. That is because they were never intended to be used for finding/understanding proofs, they were intended for facilitating proofs about proofs.

I will give you a sketch.

Lemma. ¬◻(A→B) ⊢ ◊A, ◊¬B.

⊢ ¬A→(A→B)        Propositional logic
⊢ ◻¬A→◻(A→B)      Necessitation and K
¬◻(A→B) ⊢ ¬◻¬A    Propositional logic

and

⊢ B→(A→B)         Propositional logic
⊢ ◻B→◻(A→B)       Necessitation and K
¬◻(A→B) ⊢ ¬◻B     Propositional logic

This proves the lemma.

Now, if we can derive a contradiction A,¬B ⊢ C,¬C, then by propositional logic A ⊢ B (and equivalently ⊢ A→B). So to prove your claim it suffices to show ¬◻(◻P→◻Q),¬◻(◻Q→◻P) is inconsistent. Using the lemma, you get ¬◻(◻P→◻Q) ⊢ ◊◻P and ¬◻(◻Q→◻P) ⊢ ◊¬◻P. From the first part an application of axiom 5 (plus a bit of PL) gives ◊◻P ⊢ ◻P. From the second part, the definition ◊¬◻P = ¬◻◻P, and axiom 4 (plus a bit of PL) you get ¬◻◻P ⊢ ¬◻P.

This is our contradiction, so the claim is proved.

_{This is a good example why one should choose the right tool for the job. From a semantical point, a proof of your claim is quite obvious.}