To be honest, I don't quite follow what happens after 5., and how they conclude 8. without ◻φ → φ. I'm guessing that because ¬◻ψ, they can do ◇¬ψ, so they pick a world where ¬ψ is true. And because ◻φ, it must be true that φ is true in that world too. Same with φ → ψ, where from we get a contradiction. But how have we not committed to ◻φ → φ in doing this?
I'm guessing that because ¬◻ψ, they can do ◇¬ψ, so they pick a world where ¬ψ is true. And because ◻φ, it must be true that φ is true in that world too. Same with φ → ψ, where from we get a contradiction.
This is exactly right. The world v is a world where ¬ψ is true, and we know there must be such a world. Moreover, since ◻φ is true at w, and w "sees" v (that is, wRv), φ is true at v.
But how have we not committed to ◻φ → φ in doing this?
No. We are only committed to that if we say that since ◻φ is true at w, then φ is true at w, and that is not said or implied at any point. For all that is assumed in this proof, it is possible that ◻φ and ¬φ are true at w, for instance if wRw does not hold.
Note the orange (w) and (v). These are the worlds to which the statements apply. The number(s) after that are the line(s) from which the statement is derived.
Firstly we assume
◻(φ → ψ) → (◻φ → ◻ψ) is false in any world
w. Under that assumption we use that stating
~(x → y) justifies deriving both
1. ~(◻(φ → ψ) → (◻φ → ◻ψ)) (w) 2. ◻(φ → ψ) (w) 1 3. ~(◻φ → ◻ψ) (w) 1
Then similarly, the later line derives that:
4. ◻φ (w) 3 5. ~◻ψ (w) 3
Next we assert that because
ψ is not necessary in
w, therefore there exists some world accessible from
~ψ holds, we shall call one such world
v. (The notation
v is accessible from
6. wRv 5 7. ~ψ (v) 5
φ is necessary in
w, then it is true in all worlds accessible from
v is such a world...
wRv derives that
Note: This is not claiming that
φ in any one world; it is an entailment betwixt
w and its accessible world
Likewise our line 2 derivation of
w:◻(φ → ψ), and
wRv, allows us to derive that
v:(φ → ψ).
8. φ (v) 4,6 9. φ → ψ (v) 2,6
φ → ψ is equivalent to
ψ we branch out, and observe that both cases do contradict preceding derivations. (It is basically a proof by cases.)
10. ~φ (v) 9 (left branch) x 8,10 11. ψ (v) 9 (right branch) x 11,7
Now, since "all routes lead to doom" the original assumption is absurd.
◻(φ → ψ) → (◻φ → ◻ψ) cannot be false in any world
◻(φ → ψ) → (◻φ → ◻ψ) must be a theorem in modal system