Logic for Computer Scientists/Modal Logic/Axiomatics

The simplest modal logics is called ${\displaystyle K}$ and is given by the following axioms:

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

and the inference rules

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

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

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

${\displaystyle {\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 ${\displaystyle K}$ we have

${\displaystyle \square (P\land Q)\leftrightarrow (\square P\land \square Q)}$

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

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

${\displaystyle T}$ : ${\displaystyle \square A\to A}$

${\displaystyle D}$ : ${\displaystyle \square A\to \diamond A}$

${\displaystyle 4}$ : ${\displaystyle \square A\to \square \square A}$

${\displaystyle 5}$ : ${\displaystyle \diamond A\to \square \diamond A}$

${\displaystyle B}$ : ${\displaystyle A\to \square \diamond A}$

Traditionally, if one adds axioms ${\displaystyle A_{1},\cdots ,A_{n}}$ to the logic ${\displaystyle K}$ one calls the resulting logic ${\displaystyle KA_{1}\cdots A_{n}}$. Sometimes, however the logic is so well known, that it is referred to under another name; e.g. ${\displaystyle KT4}$, is called ${\displaystyle 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 ${\displaystyle R}$ of the frame. If ${\displaystyle \langle W,R\rangle }$ is a frame, then a certain axiom will be valid on ${\displaystyle \langle W,R\rangle }$, if and only if ${\displaystyle R}$ meets a certain restriction. Some restrictions are expressible by first-order logical formulae where the binary predicate ${\displaystyle R(x,y)}$ represents the reachability relation:

${\displaystyle {\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}}}$