1. In first-order theories strong enough to represent their own proof theories, a unary open formula $\text{Prv}\left(x\right)$ that is true of a natural number $n$ when $n$ encodes a formula provable in the arithmetic’s representation of proof theory. In classical logic, one can define a decidable formula $\text{Proves}\left(x,y\right)$ in the theory of Peano Arithmetic $\text{PA}$ that is true of a pair $〈m,n〉$ when $m$ encodes a proof of the formula encoded by $n$ by means of Gödel numbering. In this case, the formula $\exists x\text{Proves}\left(x,y\right)$ is true of a formula when there exists a proof of the formula encoded by $n$, giving us an operator $\text{Prv}\left(x\right)$ corresponding to provability. This is used to provide a sentence expressing the consistency of $\text{PA}$: $\text{Prv}\left(\text{⌜}0=1⌝\right)$ where $\text{⌜}0=1\text{⌝}$ is the Gödel number of the sentence $0=1$.

2. In modal logic, an interpretation of the necessity operator $\square$ in which $\square \phi$ is interpreted as ‘there exists a proof of $\phi$’. Initially suggested as an interpretation of modal logic $\text{S}4$ by mathematician Kurt Gödel (1906–1978), this interpretation formed the basis for the Gödel-McKinsey-Tarski translation of intuitionistic into $\text{S}4$. Influenced by the behaviour of the formula $\text{Prv}$ used in the proofs of Gödel’s first incompleteness theorem, this interpretation constitutes the primary interpretation of the modal logics extending $\text{GL}$, i.e., those containing Löb’s axiom:

• • $\square \left(\square \phi \to \phi \right)\to \square \phi$

Modal logics that interpret necessity in this way are known as provability logics.