# 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.

## Examples

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.

Parents:

• Mathematics

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