modal logic GL
Recall that 4 is the schema .
In any normal modal logic, implies .
The proof of this requires some theorems (http://planetmath.org/SomeTheoremSchemasOfNormalModalLogic) and meta-theorems (http://planetmath.org/SyntacticPropertiesOfANormalModalLogic) of a normal modal logic.
We start with the tautology , which an instance of the schema . Since is a theorem in any normal modal logic, is a theorem by the substitution theorem. By the syntactic property RM, is a theorem. Since is an instance of W, by law of syllogism, is a theorem.
Next, from the tautology , we have the theorem by RM. Combining this with the last theorem in the previous paragraph, we see that, by law of syllogism, , or 4, is a theorem. ∎
4 is a theorem of GL.
W is valid in a frame iff is transitive and converse well-founded.
Suppose first that the schema W is valid in , then any theorem of GL is valid in , so in particular 4 is valid in , and hence is transitive (see here (http://planetmath.org/ModalLogicS4)). We next show that is converse well-founded. Suppose not. Then there is a non-empty subset such that has no -maximal element. We want to find a model such that, for some propositional variable and some world in , , or equivalently, and . Let be the valuation such that . Pick any . Suppose . To show that , we want to show that . There are two cases:
If , then . Furthermore, since does not contain an -maximal element, there is a such that . Since , . Since , . As a result, .
If , then , so that .
Next, we want to show that . Since , and does not have an -maximal element, there is a such that . Since , . But since , .
Conversely, let be a transitive and converse well-founded frame, a model based on , and a world in . We want to show that . So suppose . Then the set is not empty. Since is converse well-founded, has a -maximal element, say . So and . Now, if , then , which means there is a such that and . But since is transitive and , we get , implying , contradicting the -maximality of . Therefore, , or . As a result, . ∎
Proposition 2 immediately implies
GL is sound in the class of transitive and converse well-founded frames.
Remark. However, unlike many other modal logics, GL is not complete in the class of transitive and converse well-founded frames. While its canonical model (hence the corresponding canonical frame) is transitive (because 4 is valid in it), it is not converse well-founded.
Instead, it can be shown that GL is complete in the restricted class of finite transitive and converse well-founded frames, or equivalently, finite transitive and irreflexive frames.