Provability predicate

[summary: A provability predicate of a theory $~$T$~$ is a formula $~$P(x)$~$ with one free variable $~$x$~$ such that:

1. If $~$T\vdash S$~$, then $~$T\vdash P(\ulcorner S \urcorner)$~$
2. $~$T\vdash P(\ulcorner A\rightarrow B \urcorner)\rightarrow (P(\ulcorner A \urcorner)\rightarrow P(\ulcorner B \urcorner))$~$
3. $~$T\vdash P(\ulcorner S \urcorner)\rightarrow P(\ulcorner P(\ulcorner S \urcorner) \urcorner)$~$ ]

A provability predicate is a formula $~$P$~$ of a theory satisfying the Hilbert-Bernais derivability conditions. If the diagonal theorem is applicable in the theory as well, then Löb's theorem and [ Gödel's second incompleteness theorem] are provable for $~$P$~$.

The Hilbert-Bernais derivability conditions are as follows:

1. (Necessitation) If $~$T\vdash S$~$, then $~$T\vdash P(\ulcorner S \urcorner)$~$
2. (Provability of modus ponens / distributive axioms) $~$T\vdash P(\ulcorner A\rightarrow B \urcorner)\rightarrow (P(\ulcorner A \urcorner)\rightarrow P(\ulcorner B \urcorner))$~$
3. (Provability of renecessitation) $~$T\vdash P(\ulcorner S \urcorner)\rightarrow P(\ulcorner P(\ulcorner S \urcorner) \urcorner)$~$

The derivability conditions are tighlty related to the axioms and rules of inference of Modal logic. In fact, the normal systems of provability are defined as those that have necessitation as a rule and the distributive axioms. %%note:They also have to be closed under substitution%% On the other hand, D3 is the axiom that defines the system [ K4], and it is also satisfied by [GL].

Examples

The verum formula $~$x=x$~$ trivially satisfies the derivability conditions.

The Standard provability predicate of arithmetic is a provability predicate.