# 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}}$ 