A fixed point of the negated arithmetic provability predicate for a computably enumerable arithmetic theory . Consistency excludes a proof of , 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.
New to topics? Read the docs here!