= Gödel sentence
{c}
{title2=$G\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G\urcorner)$}
A fixed point of the negated arithmetic provability predicate for a computably enumerable arithmetic theory $T$. Consistency excludes a proof of $G$, because a genuine proof is arithmetically verifiable and contradicts the fixed-point assertion. Omega-consistency excludes a proof of its negation. For a consistent theory extending Robinson arithmetic, this sentence is true in the standard natural numbers.
Back to article page