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:

Hierarchy of normal systems

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: