# Axiomatic proof of ⊢ □P → □◇□P in S4

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.

• Could you show us your proof of it in B? Jan 29, 2019 at 20:03
• @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. Jan 29, 2019 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. Jan 29, 2019 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
``````