 Gödel sentence

For a computably enumerable first-order theory $T$ extending Robinson arithmetic, choose the standard arithmetic arithmetical provability predicate ${\mathrm{Prov}}_T$. The diagonal lemma, carried out in the weak base theory, gives a sentence $G$ withIf $T$ is consistent, $T$ cannot prove $G$: an actual finite proof would be verifiable in the weak base, so $T$ would prove both its provability and its unprovability. There is therefore no actual proof of $G$, and the displayed equivalence, true in the standard natural numbers, shows that this canonical $G$ is true there.

If $T$ is omega-consistent, it cannot prove $\neg G$ either. Such a proof would imply the existence of a proof code for $G$, while each standard numeral can be individually verified not to be such a code. Ordinary consistency suffices for unprovability of $G$; the original argument for unprovability of its negation uses the stronger hypothesis. Requiring the fixed-point equivalence in a sound weak base is important: an arbitrary equivalence provable only in an unsound extension need not yield a true sentence.