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.

eg.

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

is a scheme which contains

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

and

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

and

$$ (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.)