# Logic for Computer Scientists/Modal Logic/Axiomatics

## AxiomaticsEdit

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?)

## Extensions of KEdit

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