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.