8

I wish to prove the following within Kripke modal logic: 

□P → ◇P

This is not a homework problem, but simply the first thing I'd like to prove. I've been able to prove more complex theorems such as □(P→Q)&◇P → ◇Q, but a straightforward proof of necessity implying possibility still eludes me.

Even a hint in the right direction is much appreciated.

Improve this question
  • 1
    Notice that in □(P→Q)&◇P → ◇Q, we know that P-worlds are Q-worlds from □(P→Q), and ◇P guarantees the existence of at least one P-world, so the whole antecedent ends up implying the existence of a Q-world (◇Q). (All of this, of course, is relative to some point in a model.) – Hunan Rostomyan Mar 30 '14 at 20:11
4

Fortunately you cannot prove it. It's invalid.

Counterexample. Consider a model M with a single world w ∈ |M| such that there is no reflexive arrow on w (i.e. ¬wRw). That gives us the fact that: (M, w) |= ▢ P, because it is vacuously true that for all worlds v ∈ |M| accessible from w (wRv), we have it that (M, v) |= P. That allows us to conclude that (M, w) |= ▢ P. But it is not the case that there is a world v ∈ |M| which is accessible from w and is such that (M, v) |= P (you know, given that there is only a single world and it is inaccessible from itself). So we cannot conclude that (M, w) |= ♢P.

The reasoning is similar to the usual one associated with the quantifiers ∀, ∃. If you have a universally quantified formula φ (i.e. ∀φ), if you interpret it in an empty domain, it will be satisfied. But the existential will not. Note also, that even if you have non-empty domain of discourse, it might still be the case that the interpretation I of φ specifically is empty, so the universal closures of φ might still evaluate to true vacuously, while the existential ones will not (given that no object falls in the extension of φ under the I).

Improve this answer
  • 1
    Could one more simply say that given a model with exactly zero worlds, then for any P □P is vacuously true but ◇P is false ? – Chris Merck Mar 30 '14 at 20:14
  • Haha, well, if that simply, you can even say: in a model with no worlds, any formula φ is valid, because for any pointed model (M, w), we have it that: (M, w) |= φ. Sure! – Hunan Rostomyan Mar 30 '14 at 20:18
  • What's the motivation for choosing this behaviour here. I can see that's how one would want to define quantifiers, but on its own that doesn't mean that one should use their definition for defining modal operators. Are there any major consequences of this decision? Why can't change the definition of □ (and/or ◇) with respect to the possible worlds to let the OPs statement be true? – Lucas Mar 30 '14 at 20:49
  • In other words, when you say "If you have a universally quantified formula φ (i.e. ∀φ), if you interpret it in an empty domain, it will be satisfied" why isn't this reification of the possible worlds - taking them as more real than the modal operators which are the primary concern. – Lucas Mar 30 '14 at 20:52
  • @Lucas The reason is that the quantifiers are an essential part of the usual semantics of the modal operators. Now, as Shane suggested in the comment above, you can simply add restrictions on the accessibility relation to reflect your intuitions about the relation between boxes and diamonds. For example, if you want necessity implying possibility, then you want to add axiom D to the core. Say you're working with knowledge (or provability), you adopt axiom 4 to capture the intuition that: if you know (or have proved) P, then you know (or have proved) that you know (or have proved) P. And so on – Hunan Rostomyan Mar 30 '14 at 21:11
4

Another hint in the right direction: It's not true that "the weakest logic that proves that formula is T". Rather the weakest logic with that property is D, whose frames F = W, R (I miss LaTex so badly here!) are serial, that is for every member w of W there is a w' from W such that wRw'. Indeed, the OP's formula characterizes the class of serial frames: A frame is serial iff the formula is valid in that frame (valid in every model based on that frame). D is a proper sublogic of T since every T-frame is a D-frame but the T-Axiom is not D-valid.

Improve this answer
  • Indeed, D is the minimal. As regards LaTeX, especially for modal logic, some means of drawing directed graphs would make things so much easier to explain. For logic in general, I suggest you establish intimate acquaintance with the html character set. The <sub><sup><kbd> tags also come in handy. Good luck. – Hunan Rostomyan Mar 30 '14 at 21:27
  • Thanks @sequitur for catching my mistake. Every reflexive frame is serial, but not vice versa. Deleted my erroneous comment above. – user5172 Mar 31 '14 at 1:05
0

[]p -> <>p is valid in serial frame only.

assume x is []p and let x have no successor.

then x has no successor means <>p is invalid for x, because x has no successor

Not relevant but:

In serial it is valid:

x[]p:Let xRy where y is Valuated (p) and so So: x<>p

Improve this answer

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.