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?