# Modal Logic: One non-transitive frame where schema 4 is invalid?

I know that schema 4 defines the class of all transitive frames, meaning that it is not valid in at least one model that is non-transitive. However, I am not sure how we would go about proving that if a frame is non-transitive then schema 4 is not valid in at least one of its models.

Such proofs usually start with something like, 'For a model M=(W, R, V) and some w, v, u in W, assume wRv and vRu but not wRu. Then assume M, w ⊨ □A. Then M, v ⊨ A.' Can we finish this proof by saying, 'Since there are no restrictions that prevent us from saying it, suppose M, u ⊨ ~A. Then M, v ⊨ □~A and M, w ⊨ □□~A, contra schema 4.'

Something about this, perhaps because its not general, doesn't sit well with me, though I can't place what. Is the above the correct way to prove that 4 is not valid in non-transitive models?

Here's a way to see why □A -> □□A is valid in all transitive frames. If □A is true at a world w, that means that A is true in every world that w can see. For every world v that w can see, w can also see everything that v sees, because of transitivity. So, if A is true at every world that w can see, then □A is true not only at w, but also at v, because w can see all that v can see. So □A is true at every world that w sees, thus □□A is true at w.

In other words, for □A -> □□A to fail at some world w, it must be that □A is true at w but □□A is not. That is, there must be some world v that w can see at which A is true but □A is not. So this must be the case:

``````(w) -----> (v) -----> (u)
A,□A       A,~□A      ~A
``````

But if the frame is transitive, then w can also see u. So the above cannot hold in a transitive frame, because if □A is true at w then A must be true at u.

I know that schema 4 defines the class of all transitive frames, meaning that it is not valid in at least one model that is non-transitive. However, I am not sure how we would go about proving that if a frame is non-transitive then schema 4 is not valid in at least one of its models.

We can prove that a schema 4 is not valid in at least one model by explicitly constructing such a model.

That is what your proof does.

The first assumption is that the frame is non-transitive (there are worlds `u,v,w` such that `wRv`, `vRu`, but `~wRu`).

The second and third assumptions builds the (counter) model for that frame by assigning valuations to proposition A (vis `w ╟ □A` and `u ╟ ~A`).

[ We can note that `w ╟ □A` and `~wRu` does not entail `u ╟ A` so there is no contradiction in these three assumption. ]

The proof by negation is then used to show that schema 4 cannot be a valid in this model, because assuming it would produce a contradiction.

[ NB: However I would have derived `u ╟ A` from `w ╟ □A→□□A`, `w ╟ □A`, `wRv`, `vRu` to contradict `u ╟ ~A`. ]

Therefore a model exists for a non-transitive frame where schema 4 is not valid.