# 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:

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

Parents:

- Modal logic
The logic of boxes and bots.