Logic for Computer Scientists/Modal Logic/Axiomatics

< Logic for Computer Scientists‎ | Modal Logic

AxiomaticsEdit

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: