Provability predicate

A prov­abil­ity pred­i­cate is a for­mula \(P\) of a the­ory satis­fy­ing the Hilbert-Ber­nais deriv­abil­ity con­di­tions. If the di­ag­o­nal the­o­rem is ap­pli­ca­ble in the the­ory as well, then Löb’s the­o­rem and Gödel’s sec­ond in­com­plete­ness the­o­rem are prov­able for \(P\).

The Hilbert-Ber­nais deriv­abil­ity con­di­tions are as fol­lows:

  1. (Ne­ces­si­ta­tion) If \(T\vdash S\), then \(T\vdash P(\ulcorner S \urcorner)\)

  2. (Prov­abil­ity of modus po­nens /​ dis­tribu­tive ax­ioms) \(T\vdash P(\ulcorner A\rightarrow B \urcorner)\rightarrow (P(\ulcorner A \urcorner)\rightarrow P(\ulcorner B \urcorner))\)

  3. (Prov­abil­ity of rene­ces­si­ta­tion) \(T\vdash P(\ulcorner S \urcorner)\rightarrow P(\ulcorner P(\ulcorner S \urcorner) \urcorner)\)

The deriv­abil­ity con­di­tions are tigh­lty re­lated to the ax­ioms and rules of in­fer­ence of modal logic. In fact, the nor­mal sys­tems of prov­abil­ity are defined as those that have ne­ces­si­ta­tion as a rule and the dis­tribu­tive ax­ioms. noteThey also have to be closed un­der sub­sti­tu­tion On the other hand, D3 is the ax­iom that defines the sys­tem K4, and it is also satis­fied by GL.


The verum for­mula \(x=x\) triv­ially satis­fies the deriv­abil­ity con­di­tions.

The stan­dard prov­abil­ity pred­i­cate of ar­ith­metic is a prov­abil­ity pred­i­cate.


  • Mathematics

    Math­e­mat­ics is the study of num­bers and other ideal ob­jects that can be de­scribed by ax­ioms.