Hilbert–Bernays-Löb provability conditions

In mathematical logic, the Hilbert–Bernays-Löb provability conditions, named after David Hilbert, Paul Bernays, and Martin Löb, are a set of requirements for formalized provability predicates in formal theories of arithmetic (Smith 2007:224). These conditions are used in many proofs of Kurt Gödel's second incompleteness theorem.

Source: Wikipedia — Hilbert–Bernays-Löb provability conditions (CC BY-SA 4.0)