Let be a Kripke frame. A subframe of is a pair such that is a subset of and . A submodel of a Kripke model of a modal propositional logic PL is a triple where is a subframe of , and for each propositional variable in PL.
The most common submodel of a Kripke model is constructed by taking , where is the reflexive transitive closure of , for any . The submodel is called the submodel of generated by the world , and the subframe of generated by . A submodel of is called a generated submodel if it is generated by some world in .
For any wff and any , iff .
If , then is either or a propositional variable. Clearly, iff , or iff . If is some propositional variable , then iff iff iff and (by assumption) iff iff iff .
Next, suppose is . Then iff iff and (by assumption) iff or iff or iff .
Finally, suppose is . First let . To show , pick any such that . Then , so that , or . Since , , or , and thus . Conversely, let . To show , pick any such that . Since , so that . Furthermore . So , or , which means . ∎
iff for all .
If , then for all , so that for all and all , or for all . Conversely, if for all , then in particular (since is reflexive) for all , or for all , or . ∎
iff for all .
If , then for all based on , or , where is based on , for all by the last corollary. Since any model based on is of the form , . Conversely, suppose for all . Let be any model based on . Then is based on , and therefore . Since is arbitrary, by the last corollary, so . ∎