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.
