π“œ

Math Notes

University Mathematics

ConceptComplete

Normal Modal Logics

Normal modal logics form a well-studied family of modal logics extending the minimal normal logic K\mathbf{K}. They are characterized by additional axioms on the accessibility relation, and their model theory is tightly connected to frame properties.

The Logic K and Extensions

Definition8.4Normal Modal Logic

A normal modal logic Ξ›\Lambda is a set of modal formulas containing all propositional tautologies, the distribution axiom K:β–‘(Ο†β†’Οˆ)β†’(β–‘Ο†β†’β–‘Οˆ)\mathbf{K}: \Box(\varphi \to \psi) \to (\Box \varphi \to \Box \psi), and closed under modus ponens and necessitation (if Ο†βˆˆΞ›\varphi \in \Lambda, then β–‘Ο†βˆˆΞ›\Box \varphi \in \Lambda).

Definition8.5Common Normal Modal Logics

The principal normal modal logics are:

  • K\mathbf{K}: The minimal normal modal logic. No conditions on RR.
  • T=K+(β–‘Ο†β†’Ο†)\mathbf{T} = \mathbf{K} + (\Box \varphi \to \varphi): Reflexive frames.
  • K4=K+(β–‘Ο†β†’β–‘β–‘Ο†)\mathbf{K4} = \mathbf{K} + (\Box \varphi \to \Box \Box \varphi): Transitive frames.
  • S4=T+(β–‘Ο†β†’β–‘β–‘Ο†)\mathbf{S4} = \mathbf{T} + (\Box \varphi \to \Box \Box \varphi): Reflexive and transitive (preorder).
  • S5=S4+(Ο†β†’β–‘β—ŠΟ†)\mathbf{S5} = \mathbf{S4} + (\varphi \to \Box \Diamond \varphi): Equivalence relations.
  • GL=K+(β–‘(β–‘Ο†β†’Ο†)β†’β–‘Ο†)\mathbf{GL} = \mathbf{K} + (\Box(\Box \varphi \to \varphi) \to \Box \varphi): Provability logic.

Frame Correspondence

ExampleAxiom-Frame Correspondence

The correspondence theory relates modal axioms to first-order properties of frames: | Axiom | Name | Frame Property | |-------|------|----------------| | β–‘Ο†β†’Ο†\Box \varphi \to \varphi | T | Reflexive | | β–‘Ο†β†’β–‘β–‘Ο†\Box \varphi \to \Box \Box \varphi | 4 | Transitive | | β—ŠΟ†β†’β–‘β—ŠΟ†\Diamond \varphi \to \Box \Diamond \varphi | 5 | Euclidean | | β–‘(β–‘Ο†β†’Ο†)β†’β–‘Ο†\Box(\Box \varphi \to \varphi) \to \Box \varphi | GL | Transitive + well-founded | | β–‘β—ŠΟ†β†’β—Šβ–‘Ο†\Box \Diamond \varphi \to \Diamond \Box \varphi | .2 | Directed (confluent) |

RemarkSahlqvist Correspondence

The Sahlqvist correspondence theorem provides an algorithm: for a wide class of modal formulas (Sahlqvist formulas), one can effectively compute the first-order frame condition. Every Sahlqvist formula is canonical (valid on its canonical frame), and the corresponding logic is complete with respect to its frame class.

Definition8.6Canonical Model

The canonical model MΞ›=(WΞ›,RΞ›,VΞ›)\mathcal{M}_\Lambda = (W_\Lambda, R_\Lambda, V_\Lambda) for a normal modal logic Ξ›\Lambda has WΞ›=W_\Lambda = the set of all maximally Ξ›\Lambda-consistent sets, wRΞ›vwR_\Lambda v iff {Ο†:β–‘Ο†βˆˆw}βŠ†v\{\varphi : \Box\varphi \in w\} \subseteq v, and VΞ›(p)={w:p∈w}V_\Lambda(p) = \{w : p \in w\}. The canonical model is used to prove completeness theorems.