# How to prove □ φ ↔ ◊ □ φ

I am looking for a proof of the formula □ φ ↔ ◊ □ φ (a theorem in modal logic S5) How can this theorem be proven from the axioms of modal logic? It makes some intuitive sense to me, as something that is necessary must be possible, but how can you step by step prove s5's contra positive? Specifically from ◊ □ φ to □ φ as the reverse is a trivial possibility introduction but in this direction it seems explosive with □ □ φ?

• I don't understand the last sentence, but it may be my fault. I upvoted because I'm reasonably intrigued what the answer is, though I imagine it's quite obvious to some
– user63756
Commented Dec 11, 2022 at 8:53

As you say, □φ → ◇□φ is straightforward, since S5 contains the T axiom,

``````T:     □ψ → ψ
``````

So by substutiting ¬□φ for ψ

``````□¬□φ → ¬□φ
``````

hence by contraposition

``````□φ → ¬□¬□φ
``````

and hence by the equivalence of ◇φ with ¬□¬φ

``````□φ → ◇□φ
``````

To get the converse, ◇□φ → □φ, start with axiom 5,

``````5:   ◇ψ → □◇ψ
``````

Substituting ¬φ for ψ

``````◇¬φ → □◇¬φ
``````

hence by contraposition

``````¬□◇¬φ → ¬◇¬φ
``````

and hence by the equivalence of ◇φ with ¬□¬φ and of □φ with ¬◇¬φ and double negation elimination

``````◇□φ → □φ
``````

In general with S5, when you have an expression with iterated modal operators, you can always simplify it down to its rightmost operator. □□φ and ◇□φ are both equivalent to □φ. Also, □◇φ and ◇◇φ are both equivalent to ◇φ. It does not entail any kind of explosion.