Mathematics.

formal logic

Modal Logic

Mathematical Logic25 minDifficulty3 out of 10

You should know: propositional logic

Overview

Modal logic extends propositional (or predicate) logic with operators expressing modes of truth beyond plain true/false — most commonly necessity (□, 'it is necessarily the case that') and possibility (◇, 'it is possibly the case that'), which are interdefinable via ◇φ ≡ ¬□¬φ. Its standard semantics, due to Saul Kripke, interprets formulas relative to a set of 'possible worlds' connected by an accessibility relation R, where □φ is true at a world w if φ is true at every world accessible from w, and ◇φ is true at w if φ is true at some accessible world. Different constraints on the accessibility relation (reflexive, transitive, symmetric, etc.) yield different modal systems — K (no constraints), T (reflexive), S4 (reflexive + transitive), and S5 (equivalence relation) — each validating different additional axioms. Beyond necessity/possibility, the same Kripke-world framework underlies temporal logic (□ = 'always,' ◇ = 'eventually'), epistemic logic (□ = 'it is known that'), and deontic logic (□ = 'it is obligatory that').

Intuition

Modal logic formalizes the difference between 'true' and 'true no matter what' by imagining a whole landscape of alternative possible worlds, connected to each other by an accessibility relation representing which worlds are 'reachable' or 'relevant' from any given one — □φ says φ holds in every world you can reach, while ◇φ says φ holds in at least one reachable world. The genius of this framework is its flexibility: swap in a different reading of 'accessible world' and the exact same machinery models entirely different notions — 'accessible' can mean 'a moment in time still to come' (temporal logic, □ = always in the future), 'a scenario consistent with what an agent knows' (epistemic logic, □ = known), or 'a scenario satisfying all obligations' (deontic logic, □ = obligatory) — with the choice of accessibility relation's properties (reflexive? transitive? symmetric?) determining which extra axioms, like □φ→φ, become valid.

Formal Definition

Definition

Modal logic adds □ and ◇ to propositional logic, with Kripke semantics over worlds W and accessibility relation R ⊆ W×W:

◊φ≡¬□¬φ\Diamond \varphi \equiv \neg \Box \neg \varphi
Interdefinability of the modal operators
M,w⊨□φ  ⟺  ∀v (wRv  ⟹  M,v⊨φ)M, w \vDash \Box\varphi \iff \forall v\, (wRv \implies M,v \vDash \varphi)
Kripke truth condition for necessity
Axiom T: □φ→φ(valid iff R is reflexive)\text{Axiom T: } \Box\varphi \rightarrow \varphi \quad \text{(valid iff R is reflexive)}
T axiom (reflexivity)
Axiom 4: □φ→□□φ(valid iff R is transitive)\text{Axiom 4: } \Box\varphi \rightarrow \Box\Box\varphi \quad \text{(valid iff R is transitive)}
Axiom 4 (transitivity, gives system S4)

Worked Examples

  1. By definition, ◇φ is true at w iff φ holds at some accessible world.

    M,w⊨◊φ  ⟺  ∃v (wRv∧M,v⊨φ)M,w \vDash \Diamond\varphi \iff \exists v\, (wRv \land M,v \vDash \varphi)

  2. □¬φ is true at w iff ¬φ holds at every accessible world, i.e. φ fails everywhere accessible.

    M,w⊨□¬φ  ⟺  ∀v (wRv  ⟹  M,v⊭φ)M,w \vDash \Box\neg\varphi \iff \forall v\, (wRv \implies M,v \nvDash \varphi)

  3. Negating: ¬□¬φ holds iff it's not the case that φ fails everywhere accessible, i.e. φ holds somewhere accessible — exactly the condition for ◇φ.

    M,w⊨¬□¬φ  ⟺  ∃v (wRv∧M,v⊨φ)M,w \vDash \neg\Box\neg\varphi \iff \exists v\, (wRv \land M,v \vDash \varphi)

Answer: Both conditions coincide exactly, confirming ◇φ ≡ ¬□¬φ.

Practice Problems

Difficulty 2/10

In epistemic logic, if □ is read as 'agent knows that,' how would you read ◇φ?

Difficulty 3/10

What extra structural property does the accessibility relation need for the axiom φ → □◇φ to be valid, and which modal system typically includes this?

Difficulty 4/10

Explain why system S5 (accessibility relation is an equivalence relation) makes □ and ◇ behave like universal/existential quantifiers over a single fixed set of worlds, collapsing iterated modalities like □◇φ to ◇φ.

Quiz

In Kripke semantics, □φ is true at world w if:
The modal axiom □φ → φ (Axiom T) corresponds to the accessibility relation being:
The same modal (□, ◇) framework, with a different reading of the accessibility relation, is used in all of the following EXCEPT:

Summary

  • Modal logic adds necessity (□) and possibility (◇) to propositional logic, interdefinable via ◇φ ≡ ¬□¬φ.
  • Kripke semantics interprets □φ as truth in every world accessible from the current one, with different constraints on the accessibility relation (reflexive, transitive, symmetric) yielding systems K, T, S4, S5.
  • The same framework underlies temporal, epistemic, and deontic logic by reinterpreting what 'accessible world' means.

References

  1. WebsiteWikipedia — Modal logic