Normal system of provability logic

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:

  1. Has necessitation as a rule of inference. That is, if \(L\vdash A\) then \(L\vdash \square A\).

  2. Has modus ponens as a rule of inference: if \(L\vdash A\rightarrow B\) and \(L\vdash A\) then \(L\vdash B\).

  3. Proves all tautologies of propositional logic.

  4. Proves all the distributive axioms of the form \(\square(A\rightarrow B)\rightarrow (\square A \rightarrow \square B)\).

  5. 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:

Hierarchy of normal systems

Those systems are:

  • The system K

  • The system K4

  • The system GL

  • The system T

  • The system S4

  • The system B

  • The system S5