Last modified on 13 July 2009, at 14:09

Logic for Computer Scientists/Modal Logic/Axiomatics

AxiomaticsEdit

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 KEdit

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. K T 4, 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}