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