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.
This diagonal sentence says that any proof of itself has a no-later proof of its negation. A proof of contradicts finite verification that no earlier opposite proof exists. A proof of its negation, together with finite verification that no earlier proof of exists, proves the displayed universal condition and hence . Thus consistency alone excludes both proofs, strengthening the original omega-consistency form of incompleteness.

Articles by others on the same topic (0)

There are currently no matching articles.