= Gödel sentence
{c}
{title2=$G\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G\urcorner)$}
For a <computably enumerable> <first-order theory> $T$ extending <Robinson arithmetic>, choose the standard arithmetic <arithmetical provability predicate> $\operatorname{Prov}_T$. The <diagonal lemma>, carried out in the weak base theory, gives a sentence $G$ with
$$
\mathsf Q\vdash G\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G\urcorner).
$$
If $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.
Back to article page
