0

Proof

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?

  • 1
    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
1

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.

0

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).

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.