# How does the proof of ◻(φ → ψ) → (◻φ → ◻ψ) not presuppose ◻φ → φ? 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?

• Basically, step (8) is justified by the following: if our current world w satisfies ◻φ, and wRv, then v satisfies φ. This is true essentially trivially: it's the definition of ◻ in the context of Kripke semantics. However, this does not amount to saying "If our current world w satisfies ◻φ then our current world w satisfies φ" (which would amount to a commitment to ◻φ → φ). If this helps clarify things I can expand it into an answer. – Noah Schweber May 11 '20 at 19:31

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 `x` and `~y`.

`````` 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 `w` where `~ψ` holds, we shall call one such world `v`. (The notation `wRv` states `v` is accessible from `w`).

`````` 6. wRv                            5
7. ~ψ                         (v) 5
``````

Now because `φ` is necessary in `w`, then it is true in all worlds accessible from `w`. Since `v` is such a world... `w:◻φ` and `wRv` derives that `v:φ`.

Note: This is not claiming that `◻φ` entails `φ` in any one world; it is an entailment betwixt `w` and its accessible world `v` .

Likewise our line 2 derivation of `w:◻(φ → ψ)`, and `wRv`, allows us to derive that `v:(φ → ψ)`.

`````` 8. φ                         (v) 4,6
9. φ → ψ                     (v) 2,6
``````

Now since `φ → ψ` is equivalent to `~φ` or `ψ` 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.

So `◻(φ → ψ) → (◻φ → ◻ψ)` cannot be false in any world `w`.

Therefore `◻(φ → ψ) → (◻φ → ◻ψ)` must be a theorem in modal system `K` (Krippke).