Question

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 □ □ φ?

Answer 1

To prove the theorem □ φ ↔ ◇ □ φ in modal logic S5, one can rely on necessary axioms, necessary and sufficient conditions, and rules of inference like modus ponens and modus tollens. Assuming that it is possible that φ is necessary, one can infer that it is necessary that φ is possible, and thus that φ is necessary.

Step-by-step explanation:

The proof for the theorem □ φ ↔ ◇ □ φ in modal logic S5 claims that if something is possibly necessary (◇ □ φ), then it is necessary (□ φ). The proof can be derived using the S5 axioms and rules of modal logic, which include understanding necessary and sufficient conditions as well as rules of inference such as modus ponens and modus tollens. Let's consider a step-by-step proof utilizing these principles.

We start with the assumption that ◇ □ φ (it is possible that φ is necessary). In S5, an axiom states that if something is possible, then it is necessarily possible (if ◇ φ, then □ ◇ φ). So from our assumption, we can infer □ ◇ □ φ (it is necessary that it is possible that φ is necessary). Now, given that necessity distribution axiom (□ (p → q) → (□ p → □ q)) and modal axiom T (□ p → p), we can argue that if it is necessary that φ is possible, then φ is necessary.