Nor­mal sys­tem of prov­abil­ity 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⊢A$ then $L⊢\square A$.

2. Has modus ponens as a rule of inference: if $L⊢A\to B$ and $L⊢A$ then $L⊢B$.

3. Proves all tautologies of propositional logic.

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

5. It is closed under substitution. That is, if $L⊢F\left(p\right)$ then $L⊢F\left(H\right)$ 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⊢\square (A_1\wedge ...\wedge A_n)\leftrightarrow (\square A_1\wedge ...\wedge \square A_n)$

• Suppose $L⊢A\to B$. Then $L⊢\square A\to \square B$ and $L⊢\diamond A\to \diamond B$.

• $L⊢\diamond A\wedge \square B\to \diamond (A\wedge B)$

First substitution theorem

Normal systems also satisfy the first substitution theorem.

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

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