Between the modal systems of provability, the normal systems distinguish themselves by exhibiting nice properties that make them useful to reason.

A normal system of provability is defined as satisfying the following conditions:

- Has
**necessitation**as a rule of inference. That is, if $~$L\vdash A$~$ then $~$L\vdash \square A$~$. - Has
**modus ponens**as a rule of inference: if $~$L\vdash A\rightarrow B$~$ and $~$L\vdash A$~$ then $~$L\vdash B$~$. - Proves all
**tautologies**of propositional logic. - Proves all the
**distributive axioms**of the form $~$\square(A\rightarrow B)\rightarrow (\square A \rightarrow \square B)$~$. - It is
**closed under substitution**. That is, if $~$L\vdash F(p)$~$ then $~$L\vdash F(H)$~$ for every modal sentence $~$H$~$.

The simplest normal system, which only has as axioms the tautologies of propositional logic and the distributive axioms, it is known as the [ K system].

## Normality

The good properties of normal systems are collectively called **normality**.

Some theorems of normality are:

- $~$L\vdash \square(A_1\wedge … \wedge A_n)\leftrightarrow (\square A_1 \wedge … \wedge \square A_n)$~$
- Suppose $~$L\vdash A\rightarrow B$~$. Then $~$L\vdash \square A \rightarrow \square B$~$ and $~$L\vdash \diamond A \rightarrow \diamond B$~$.
- $~$L\vdash \diamond A \wedge \square B \rightarrow \diamond (A\wedge B)$~$

## First substitution theorem

Normal systems also satisfy the first substitution theorem.

(

First substitution theorem) Suppose $~$L\vdash A\leftrightarrow B$~$, and $~$F(p)$~$ is a formula in which the sentence letter $~$p$~$ appears. Then $~$L\vdash F(A)\leftrightarrow F(B)$~$.

## The hierarchy of normal systems

The most studied normal systems can be ordered by extensionality:

Those systems are:

- The system K
- The system K4
- The system GL
- The system T
- The system S4
- The system B
- The system S5