Semantics for normal modal logic: Kripke models

Normal modal logics can be given a nice semantics by means of Kripke models, also known as possible worlds semantics.

Probably the most important reason for the popularity of possible-worlds semantics is that common modal axioms correspond exactly to certain algebraic properties of Kripke models in the following sense: an axiom is valid in a model $M$ if and only if the alternativeness relation of $M$ satisfies some algebraic condition. (In fact, the correspondence holds on a higher abstraction level, the level of frames, consult [vB84] for details.) In particular:

• (T) holds iff $R$ is reflexive
• (D) holds iff $R$ is serial
• (4) holds iff $R$ is transitive
• (5) holds iff $R$ is Euclidean
• (G) holds iff $R$ is directed

The common normal modal logics can be characterized by appropriate classes of Kripke models. In the following theorem, a Kripke model is said to be reflexive iff its accessibility relation is reflexive, and so on.

The common normal propositional modal logics are conservative extensions of classical logic: if a formula $\alpha$ does not contain any occurrence of the modal operator then it is provable in a system mentioned in the previous theorem if and only if it is provable in the propositional calculus.