The System S5

The System S5

The axioms of S5 are these:

If (the conditional) if p then q is necessary, then if it is necessary that p, then it is necessary that q.
If it is necessary that p, then p is true.
If it is possible that p, then it is necessary that it is possible that p.

The axioms all turn out true if we analyze necessity as `truth in all possible worlds' and possibility as `truth in some possible world'. The Rule of Inference is: if p is a theorem, so is necessarily p.

Formal Presentation of S5 (for Graphical Browsers)

Modal logicians use the following notation to symbolize the English:

In terms of this notation, the S5 axioms may be formalized as follows:

The Rule of Inference is notated as follows:

When studying this formal system, logicians are not only interested in discovering the theorems derivable from these axioms and rule, but also in developing abstract models in which the axioms and theorems all turn out true.