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.
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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