Modal logic

Modal logic is the family of formal systems that extend propositional logic and predicate logic with modal operators expressing necessity (□, 'it is necessary that') and possibility (◇, 'it is possible that'). Where classical logic is concerned with what is actually true, modal logic is concerned with what must be true, what could be true, and what is true in alternative circumstances.

The modern formalization of modal logic is due to Saul Kripke, who introduced the semantics of possible worlds: a sentence □P is true at a world w just when P is true at all worlds accessible from w; ◇P is true at w just when P is true at some accessible world. The accessibility relation — which worlds count as 'possible' relative to which others — encodes the specific modal logic: reflexive accessibility yields the system T, transitive yields S4, and transitive + symmetric yields S5.

Modal logic is not a single system but a toolkit. Epistemic logic models knowledge and belief (□ becomes 'the agent knows'). Deontic logic models obligation and permission. Temporal logic models change over time. Each application fixes the accessibility relation differently and thereby produces a different logic of the target domain.

The computational properties of modal logics vary dramatically. Basic modal logic over Kripke frames is decidable and has the finite model property, but many extensions — particularly those combining modalities or adding fixed-point operators — become undecidable or have non-elementary complexity. This makes modal logic a testing ground for the tradeoff between expressiveness and computational tractability.

Modal logic is the formal study of alternative possibilities — and any system that plans, predicts, or reasons about counterfactuals is doing modal logic, whether it knows it or not. The fact that most AI systems lack explicit modal reasoning is not a simplification; it is a blind spot that becomes costly the moment the system must distinguish between what is true and what must remain true.