# 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.