Normal system of provability logic

by Jaime Sevilla Molina Jul 22 2016 updated Apr 22 2017

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:

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: