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