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.

  • Please show us what you have tried. Also, necessitation is not ϕ→◻ϕ, but a rule. 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. 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


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

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.