# On which frames is the modal system KW valid?

KW is defined as K + the axiom W: □(□p→p)→□p. It is said to be valid on all finite transitive and irreflexive frames. Another way to interpret my question is, what exactly does finite mean here? Let's try to falsify this axiom without the finite restriction.

``````1. □(□p→p) ∧ ¬□p in w0
2. □(□p→p) ∧ ◇¬p in w0
3. ¬p ∧ □p→p in w1
4. ¬p ∧ ¬p→¬□p in w1
5. ¬p ∧ ¬□p in w1
6. ¬p ∧ ◇¬p in w1
7. ¬p in w2
``````

So if the frames were only transitive and irefflexive, this would serve as a countermodel for KW. So we must arrive to a contradiction through this property of being finite, or else W is falsifiable. How exactly does that happen?

Now I have "a hunch" as to why this could happen, and will only include it as a guess. Let's take a frame {W,R} in which W only has w0, w1 and w2, where no frame can see itself and we have transitivity, i.e, w0Rw1, w1Rw2, then w0Rw2. From □(□p→p) we get □(¬□p ∨ p), so by applying K9 we get □¬□p ∨ ◇p, i.e ¬◇p→□◇¬p, i.e □¬p→□◇¬p. Now, since ¬p belongs to every world that w0 can see, □¬p is a truth of w0, and by modus ponens, □◇¬p. By transitivity, w0Rw2 ◇¬p is a truth of w2 as well, so there must be a world w3 in which -p is true, which can't be the case, since W only has w0,w1 and w2.

Let me try to show that □(□p→p)→□p is true in all models given a frame {W,R} where W is {w0,w1,w2} and R is transitive and irreflexive:

``````w1: p is false
w2: p is false
Since p is false in w1, □p is false in w0.
Since p is false in w2, □p is false in w1. Therefore, □p→p is true in w1 by PC.
Since w2 does not see any worlds, □p is true at w2. □p→p is false at w2.
Since (□p→p) is not true in all worlds that w0 sees, □(□p→p) is false at w0. Since □p is false as well, □(□p→p)→□p is true in w0.
Since (□p→p) is not true in all worlds that w1 sees, □(□p→p) is false at w1. Since □p is false as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.

w1: p is true
w2: p is false
Since p is false in w2, □p is false in w0, because w0 sees w2 due to transitivity.
Since p is false in w2, □p is false in w1. Therefore, □p→p is true in w1 by PC.
Since w2 does not see any worlds, □p is true at w2. □p→p is false at w2.
Since (□p→p) is not true in all worlds that w0 sees, □(□p→p) is false at w0. Since □p is false as well, □(□p→p)→□p is true in w0.
Since (□p→p) is not true in all worlds that w1 sees, □(□p→p) is false at w1. Since □p is false as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.

w1: p is false
w2: p is true
Since p is false in w1, □p is false in w0.
Since p is true in w2, □p is true in w1. Therefore, □p→p is false in w1.
Since w2 does not see any worlds, □p is true at w2. □p→p is true at w2.
Since (□p→p) is not true in all worlds that w0 sees, □(□p→p) is false at w0. Since □p is false as well, □(□p→p)→□p is true in w0.
Since (□p→p) is true in all worlds that w1 sees, □(□p→p) is true at w1. Since □p is true as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.

w1: p is true
w2: p is true
Since p is true in w1 and w2, □p is true in w0.
Since p is true in w2, □p is true in w1. Therefore, □p→p is true in w1.
Since w2 does not see any worlds, □p is true at w2. □p→p is true at w2.
Since (□p→p) is true in all worlds that w0 sees, □(□p→p) is true at w0. Since □p is true as well, □(□p→p)→□p is true in w0.
Since (□p→p) is true in all worlds that w1 sees, □(□p→p) is true at w1. Since □p is true as well, □(□p→p)→□p is true in w1.
Since w2 does not see any worlds, both □(□p→p) and □p are true, so □(□p→p)→□p is true in w2.
``````

Therefore, given a frame {W,R} where W is {w0, w1, w2}, R is transitive and irreflexive and R: {w0Rw1, w1Rw2, w0Rw2}, □(□p→p)→□p is valid on that frame. That's my hunch about what "finite" could mean, but I would really like to hear a proper answer.

• I think you have it right. The finite condition is also commonly expressed as 'conversely well-founded' and means that there are no infinite ascending sequences of PWs. – Bumble Jun 17 '20 at 0:36

## 1 Answer

A viewpoint I would suggest as a way to intuitively internalise the frame properties of KW system is to notice that it is equivalent to Gödel-Löb provability logic (GL), and necessity is conceptually a correlate of provability.

GL has several interpretations, in particular, arithmetical and computational. Besides, we may visualise it as realising our general notion of (formal) proof and the conditions on the accessibility relation R are fixed accordingly.

We can take 'p is true' as 'p is true simpliciter' and '□p is true' as 'p is provably true' in a proof system S, coincidence of which cannot be assumed. Then, accessibility among nodes (possible worlds) turns out to be possibility of transitions among proof states presenting truth simpliciter and provable truth (with respect to S). Hence the frame properties:

• A statement is required to not invoke itself as a justification of itself. That is, the proof states have to be connected non-reflexively, otherwise petitio principii would follow.

• Obviously, the proof states (or steps) must be connected in a transitive fashion.

• A proof must comprise finite number of states (like algorithm steps) to be admissible. The chain of states must end at some node, namely, it has to be well-capped (converse well-founded).