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. $KT4$, 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}}$