Provability predicate

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⊢S$, then $T⊢P(┌S┐)$
2. (Provability of modus ponens / distributive axioms) $T⊢P(┌A\to B┐)\to \left(P\right(┌A┐)\to P(┌B┐\left)\right)$
3. (Provability of renecessitation) $T⊢P(┌S┐)\to P(┌P(┌S┐)┐)$

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. ^[1] 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.

1. ^{^︎}

   They also have to be closed under substitution