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 $◻(X\to Y)\to (◻X\to ◻Y)$

and the inference rules

• Modus Ponens Rule: Conclude $Y$ from $X$ and $X\to Y$
• Necessitation Rule: Conclude $◻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 $\mathrm{\varnothing }$.

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

$\begin{array}{ccc}& \text{Tautology: }& P\to (Q\to (P\wedge Q))\\ & \text{Necessitation: }& ◻(P\to (Q\to (P\wedge Q)))\\ & \text{Modal axiom:}& ◻(P\to (Q\to (P\wedge Q)))\to (◻P\to ◻(Q\to (P\wedge Q)))\\ & \text{Modus ponens: }& ◻P\to ◻(Q\to (P\wedge Q))\\ & \text{Modal axiom:}& ◻(Q\to (P\wedge Q))\to (◻Q\to ◻(P\wedge Q))\\ & \text{Classical arg: }& ◻P\to (◻Q\to ◻(P\wedge Q))\\ & \text{Classical arg: }& (◻P\wedge ◻Q)\to ◻(P\wedge Q)\end{array}$

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

$◻(P\wedge Q)\leftrightarrow (◻P\wedge ◻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$ : $◻(X\to Y)\to (◻X\to ◻Y)$

$T$ : $◻A\to A$

$D$ : $◻A\to \diamond A$

$4$ : $◻A\to ◻◻A$

$5$ : $\diamond A\to ◻\diamond A$

$B$ : $A\to ◻\diamond A$

Traditionally, if one adds axioms $A_1,\cdots ,A_n$ to the logic $K$ one calls the resulting logic $K{A}_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 $⟨W,R⟩$ is a frame, then a certain axiom will be valid on $⟨W,R⟩$, 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{array}{ccc}T:& \text{Reflexive}& \mathrm{\forall }w\text{:}R(w,w)\\ D:& \text{Serial}& \mathrm{\forall }w\mathrm{\exists }{w}^{\prime }:R(w,w^{\prime })\\ 4:& \text{Transitive}& \mathrm{\forall }s,t,u:(R(s,t)\wedge R(t,u))\to R(s,u)\\ 5:& \text{Euclidean}& \mathrm{\forall }s,t,u:(R(s,t)\wedge R(s,u))\to R(t,u)\\ B:& \text{Symmetric}& \mathrm{\forall }w,w^{\prime }:R(w,w^{\prime })\to R(w^{\prime },w)\end{array}$