# Logic for Computer Scientists/Modal Logic/Axiomatics

## Axiomatics[edit]

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 K[edit]

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: