# What is the counterexample in modal system K for "⬜A ➡A"?

As I understand it from Modal Logic 2.1 - the systems M, B, S4 & S5, I should not be able to show "⬜A ➡A" in modal logic K. The following truth tree seems to confirm this, if I did it correctly:

There is no contradiction in w0 and I have no possibly operator allowing me to continue the tree into a new world. Because the accessibility relation is not reflexive in K, I cannot derive A in w0 to reach a contradiction that I would be able to in modal system M.

The truth tree remains open, implying that I cannot show "⬜A ➡A" in K. However, when I try to find a counterexample in K, I am stuck.

Let v be the valuation function. There are two possibilities:

1. v(A) = 1. If that is the case then "⬜A" is 1 and so is "A" which means the conditional is true. So that valuation does not lead to a contradiction.
2. v(A) = 0. If that is the case then "⬜A" is 0 and so is "A" which means the conditional is again true.

I don't see how I can construct a counterexample in K. That counterexample should also work as a counterexample in M where this can be derived. Perhaps being invalid does not mean I can always create a counterexample, but without the counterexample is it really invalid?

Reference

Kane B channel, Modal logic 2.1 - the systems M, B, S4 & S5 https://youtu.be/VRVX7B5Iw14

• A valuation function in modal logic doesn't simply assign 1 or 0 to A, but rather it assigns 1 or 0 relative to a world. In w0, for example, ⬜A could get 1 while A gets 0, as your tree shows possible.
– E...
Commented Nov 17, 2018 at 16:22
• The semantics is v(□A,w)=T iff for every world w′ in W such that wRw' we have : v(A,w′)=T. If R is not reflexive, this means that not w0Rw0. Thus, as per previous comment, the fact that A is false in w0 does not contradict the fact that □A is true in it, because from this we cannot infer that A is true in w0. Commented Nov 17, 2018 at 16:41
• @MauroALLEGRANZA R is not reflexive and we only have world w0, so R is empty. I assume what you are saying is □A is true, A is false (because of ~A) and so the conditional is false and that would be the counterexample. Commented Nov 17, 2018 at 16:58

You are reading □A as a claim "A is true in every possible world" and inferring "A is true in the actual world" would be a logical consequence of that.

Rather, in Kripke's semantics, □A is read "A is true in every accessible world (with respect to a current world)". The axioms of the various modal logic systems establish requisite properties of the accessibility relations. In system K there is no axiom requiring any world to access itself (i.e., an accessibility relation may not be reflexive in K).

So in K it is allowed that you may have a frame where a world (w0) does not access itself, A is false there, but true in every world that is accessible from there. That is the counter example. That is also your diagram.

• I don't think there are any accessible worlds, only the actual world. I can see how A is false in the actual world (w0). Would you have a reference with more information on this position? +1 Commented Nov 18, 2018 at 1:18
• The diagram does not indicate how many (if any) worlds are accessible; there may be none, but we cannot infer it. It does indicates that in all of them that there are, A will be true; ie □A . Since A is not true in w0 itself, this indicates that w0 cannot access w0. Commented Nov 18, 2018 at 12:37
• My suspicion is that we cannot work with counterexamples in modal logic. But you raise up another question. If I cannot draw a world in a truth tree does that mean that no other world than w0 exists? I assume not, but I don't know what the literature says on this question. From my perspective on this tree there are no other worlds and because the accessibility relationship does not allow reflexivity, it is empty. Commented Nov 18, 2018 at 15:08
• No. The rule, that you cannot draw another world from a necessary statement, is by reason that the necessity does not guarantee that there are any witnesses. That is not to say that there are none. Commented Nov 18, 2018 at 22:00