# Normal system of provability logic

Between the modal sys­tems of prov­abil­ity, the nor­mal sys­tems dis­t­in­guish them­selves by ex­hibit­ing nice prop­er­ties that make them use­ful to rea­son.

A nor­mal sys­tem of prov­abil­ity is defined as satis­fy­ing the fol­low­ing con­di­tions:

1. Has ne­ces­si­ta­tion as a rule of in­fer­ence. That is, if $$L\vdash A$$ then $$L\vdash \square A$$.

2. Has modus po­nens as a rule of in­fer­ence: if $$L\vdash A\rightarrow B$$ and $$L\vdash A$$ then $$L\vdash B$$.

3. Proves all tau­tolo­gies of propo­si­tional logic.

4. Proves all the dis­tribu­tive ax­ioms of the form $$\square(A\rightarrow B)\rightarrow (\square A \rightarrow \square B)$$.

5. It is closed un­der sub­sti­tu­tion. That is, if $$L\vdash F(p)$$ then $$L\vdash F(H)$$ for ev­ery modal sen­tence $$H$$.

The sim­plest nor­mal sys­tem, which only has as ax­ioms the tau­tolo­gies of propo­si­tional logic and the dis­tribu­tive ax­ioms, it is known as the K sys­tem.

## Normality

The good prop­er­ties of nor­mal sys­tems are col­lec­tively called nor­mal­ity.

Some the­o­rems of nor­mal­ity are:

• $$L\vdash \square(A_1\wedge ... \wedge A_n)\leftrightarrow (\square A_1 \wedge ... \wedge \square A_n)$$

• Sup­pose $$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 sub­sti­tu­tion theorem

Nor­mal sys­tems also satisfy the first sub­sti­tu­tion the­o­rem.

(First sub­sti­tu­tion the­o­rem) Sup­pose $$L\vdash A\leftrightarrow B$$, and $$F(p)$$ is a for­mula in which the sen­tence let­ter $$p$$ ap­pears. Then $$L\vdash F(A)\leftrightarrow F(B)$$.

## The hi­er­ar­chy of nor­mal systems

The most stud­ied nor­mal sys­tems can be or­dered by ex­ten­sion­al­ity:

Those sys­tems are:

• The sys­tem K

• The sys­tem K4

• The sys­tem GL

• The sys­tem T

• The sys­tem S4

• The sys­tem B

• The sys­tem S5

Parents: