modal logic S4
(T) , and
In this entry (http://planetmath.org/ModalLogicT), we show that T is valid in a frame iff the frame is reflexive.
4 is valid in a frame iff is transitive.
First, suppose is a frame validating 4, with and . Let be a model with , where a propositional variable. So . By assumption, we have . Then . This means for all such that . Since , , which means for all such that . Since , we have , or , or . Hence is transitive.
Conversely, let be a transitive frame, a model based on , and any world in . Suppose . We want to show , or for all with , we have , or for all with and all with , we have . If and , since is transitive. Then by assumption. Therefore, . ∎
As a result,
S4 is sound in the class of preordered frames.
Since any theorem in S4 is deducible from a finite sequence consisting of tautologies, which are valid in any frame, instances of T, which are valid in reflexive frames, instances of 4, which are valid in transitive frames by the proposition above, and applications of modus ponens and necessitation, both of which preserve validity in any frame, whence the result. ∎
S4 is complete in the class of serial frames.
Since S4 contains T, its canonical frame is reflexive. We next show that the canonical frame of any consistent normal logic containing the schema 4 must be transitive. So suppose and . If , then , or by modus ponens on 4 and the fact that is closed under modus ponens. Hence , or since , or , or since . As a result, , and therefore is a preordered frame. ∎