Modal logic in the book is very different from what I thought. It turns out what I thought is modal logic is just one kind of its interpreting ($\square$ means always, and $\diamond$ means occasionally).

Basic modal logic

The language of basic modal logic is simple, just add unary connective $\square$ and $\diamond$ to propositional logic then we are done.

The model (Kripke model) of basic modal logic is specified by

  • A world set $W$
  • A relation $R$ on $W$
  • A function $L : W → \mathcal{P}(Atoms)$, called the labelling function, basically this function give us information about which atom props are true.

Definition 5.4 on the book gives us a method on how we can use the model, basically $x \Vdash \phi$ means "$\phi$ is true in world x", and we have a bunch of structural induction rules to form such a formula.

A model $\mathcal{M} = (W, R, L)$ of basic modal logic is said to satisfy a formula if every state in the model satisfies it.

Formula scheme

All formulas which are same with each other on several top levels in their parsing tree are in the same formula scheme.


$$ \phi \rightarrow \square \phi \wedge \phi $$

is a scheme which contains

$$ p \rightarrow \square q \wedge r $$


$$ q \rightarrow \square p \wedge r $$


$$ (p \vee q) \rightarrow \square (r \vee s) \wedge (u \vee v) $$

Equivalences between modal formulas

In any world $x$ of any model $\mathcal{M}=(W,R,L)$, for all $\phi \in \Gamma$, $x ⊫ \phi \rightarrow x ⊫ \psi$, we write this as $\Gamma \models ψ$, which means $\Gamma$ of basic modal logic semantically entails a formula $ψ$ of basic modal logic.

If $\phi \models ψ$ and $\phi \models \psi$, we say $\phi \equiv \psi$.

Valid formulas

A formula $\phi$ of basic modal logic is said to be valid if it is true in every world of every model, i.e. iff $(nothing) \models \phi$ holds.

Logic engineering

(Actually this chapter made feel strange, why we re-engineer basic modal logic instead of inventing new logic? These logic seems not that similar.)