= Rosser sentence
{c}
{title2=$R\leftrightarrow\forall p(\operatorname{Prf}_T(p,R)\to\exists q\le p\,\operatorname{Prf}_T(q,\neg R))$}
This diagonal sentence says that any proof of itself has a no-later proof of its negation. A proof of $R$ contradicts finite verification that no earlier opposite proof exists. A proof of its negation, together with finite verification that no earlier proof of $R$ exists, proves the displayed universal condition and hence $R$. Thus consistency alone excludes both proofs, strengthening the original omega-consistency form of incompleteness.
Back to article page
