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

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.

(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.

• Please show us what you have tried. Also, necessitation is not ϕ→◻ϕ, but a rule. – Jishin Noben Jan 30 '19 at 2:02
• @JishinNoben I've edited to include what I've tried, but I haven't had much success at all so it isn't much. – j j jameson Jan 30 '19 at 11:01

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.