Logic for Computer Scientists/Modal Logic/Axiomatics

< Logic for Computer Scientists‎ | Modal Logic


The simplest modal logics is called   and is given by the following axioms:

  • All classical tautologies (and substitutions thereof)
  • Modal Axioms: All formulae of the form  

and the inference rules

  • Modus Ponens Rule: Conclude   from   and  
  • Necessitation Rule: Conclude   from  

A   derivation of   from a set   of formulae is a sequence of formulae, ending with  , each of it is an axiom of  , a member of   or follows from earlier terms by application of an inference rule. A \defined{  proof} of   is a   derivation of   from  .

As an example take the   proof of  :


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


Note that distributivity over disjunction does not hold! (Why?)

Extensions of KEdit

Starting from the modal logic   one can add additional axioms, yielding different logics. We list the following basic axioms:






Traditionally, if one adds axioms   to the logic   one calls the resulting logic  . Sometimes, however the logic is so well known, that it is referred to under another name; e.g.  , is called  .

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   of the frame. If   is a frame, then a certain axiom will be valid on  , if and only if   meets a certain restriction. Some restrictions are expressible by first-order logical formulae where the binary predicate   represents the reachability relation: