Logic for Computer Scientists/Modal Logic/Axiomatics

Axiomatics

The simplest modal logics is called $K$ and is given by the following axioms:

• All classical tautologies (and substitutions thereof)
• Modal Axioms: All formulae of the form $\square (X \to Y) \to (\square X \to \square Y)$

and the inference rules

• Modus Ponens Rule: Conclude $Y$ from $X$ and $X \to Y$
• Necessitation Rule: Conclude $\square X$ from $X$

A $K$ derivation of $X$ from a set $S$ of formulae is a sequence of formulae, ending with $X$, each of it is an axiom of $K$, a member of $S$ or follows from earlier terms by application of an inference rule. A \defined{$K$ proof} of $X$ is a $K$ derivation of $X$ from $\emptyset$.

As an example take the $K$ proof of $(\square P \land \square Q) \to \square (P \land Q)$:

$\begin{matrix} & \mbox{Tautology: } & P \to (Q \to (P \land Q)) \\ &\mbox{Necessitation: }& \square (P \to (Q \to(P \land Q))) \\ &\mbox{Modal axiom:}& \square (P \to (Q \to(P \land Q))) \to (\square P \to \square (Q\to (P\land Q))) \\ &\mbox{Modus ponens: } & \square P \to \square (Q \to(P \land Q)) \\ &\mbox{Modal axiom:}& \square (Q \to (P \land Q)) \to (\square Q \to \square (P\land Q)) \\ & \mbox{Classical arg: } & \square P \to (\square Q \to \square (P \land Q)) \\ & \mbox{Classical arg: } & (\square P \land \square Q) \to \square (P \land Q) \\ \end{matrix}$

There is a similar proof of the converse of this implication; hence it follows that in $K$ we have

$\square (P \land Q) \leftrightarrow (\square P \land \square Q)$

Note that distributivity over disjunction does not hold! (Why?)

Extensions of K

Starting from the modal logic $K$ one can add additional axioms, yielding different logics. We list the following basic axioms:
$K$ : $\square (X \to Y) \to (\square X \to \square Y)$

$T$ : $\square A \to A$

$D$ : $\square A \to \diamond A$

$4$ : $\square A \to \square \square A$

$5$ : $\diamond A \to \square \diamond A$

$B$ : $A \to \square \diamond A$

Traditionally, if one adds axioms $A_1, \cdots , A_n$ to the logic $K$ one calls the resulting logic $KA_1 \cdots A_n$. Sometimes, however the logic is so well known, that it is referred to under another name; e.g. $K T 4$, is called $S4$.

These logics can as well be characterised by certain classes of frames, because it is known that particular axioms correspond to particular restrictions on the reachability relation $R$ of the frame. If $\langle W,R\rangle$ is a frame, then a certain axiom will be valid on $\langle W,R\rangle$, if and only if $R$ meets a certain restriction. Some restrictions are expressible by first-order logical formulae where the binary predicate $R(x,y)$ represents the reachability relation:

$\begin{matrix} T: & \mbox{Reflexive} & \forall w \text{:} R(w,w) \\ D: & \mbox{Serial} & \forall w \exists w': R(w,w') \\ 4: &\mbox{Transitive} & \forall s,t,u: (R(s,t)\land R(t,u)) \to R(s,u) \\ 5: & \mbox{Euclidean} & \forall s,t,u: (R(s,t)\land R(s,u)) \to R(t,u) \\ B: & \mbox{Symmetric} &\forall w, w': R(w,w') \to R(w',w) \end{matrix}$