Rosser sentence ($R\leftrightarrow \forall p({\mathrm{Prf}}_T(p,R)\to \exists q\le p{\mathrm{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.

For disjoint sets numeralwise enumerated by $P,R$, finite-initial-segment and total-comparison axioms let $H$ separate the first set from the second in the theory. For a member of the first set use a positive $P$ stage and finitely many refutations of $R$. For a member of the second set use its positive $R$ stage: earlier proposed $P$ stages are all refuted by a finite bounded proof, while later stages lose to that known $R$ witness. This proves a separator without inferring arbitrary negative facts from the mere Sigma-1 form of the enumerators.

For the standard Gödel sentence and Rosser sentence, the formalized Rosser unprovability theorem and $G\leftrightarrow \mathrm{Con}(T)$ yield $T⊢G\to R$. If $T+\mathrm{Con}(T)$ is consistent, the converse is unprovable under the usual formalized incompleteness hypotheses. A proof of $R\to G$ would give $\square \neg G\to \square \neg R$. Formalized negative unprovability identifies $\neg \square \neg R$ with $\mathrm{Con}(T)$ and $\neg \square \neg G$ with $\mathrm{Con}(T+\mathrm{Con}(T))$. The strengthened theory would then prove its own consistency, contradicting the Gödel second incompleteness theorem. The consistency assumption belongs to this strictness conclusion.