As the title explains, I'm trying to give an axiomatic proof of ⊢ □P → □◇□P in S4.

This is simple to prove in B, but I'm struggling to see how it's done in S4. I'd really appreciate any help you could offer.

  • 1
    Could you show us your proof of it in B? – Jishin Noben Jan 29 '19 at 20:03
  • 1
    @JishinNoben In B one has the axiom "A → □◇A", Replace "A" with "□P" may be all one needs to show this in B. However, that axiom does not exist in S4. I don't think this can be shown in S4, but I am not sure yet how to explain why. Harry Gensler (Introduction to Logic) uses "travel tickets" to traverse these iterated modal operators and has an example on page 167 where the B axiom requires either B or S5.. I am still trying to link the travel ticket idea with these axioms. – Frank Hubeny Jan 29 '19 at 22:59
  • @FrankHubeny Thanks, but I just wanted to see whether john bercow had put some effort into it. I suppose I was too indirect. And you are right, B cannot be shown in S4, that is clear semantically/from the frame condition. – Jishin Noben Jan 29 '19 at 23:56

Here is a sketch.

(1) ⊢ □□P → ◇□P   Instance of D, which is derivable in S4
(2) ⊢ □□□P → □◇□P by (1) using necessitation, and K
(3) ⊢ □P → □◇□P   by (2), using 4 twice

How is D derivable?

(1) ⊢ □¬A → ¬A    Instance of T, which is an axiom of S4
(2) ⊢ ¬¬A → ¬□¬A  
(3) ⊢ A → ◇A
(4) ⊢ □A → ◇A     combine (3) with T
| improve this answer | |

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.