= Rosser separation by a bounded stage comparison
{c}
{title2=$H(x)=\exists y[P(x,y)\land\forall z\le y\ \neg R(x,z)]$}
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 <first-order theory>[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 formula>[Sigma-1] form of the enumerators.
Back to article page
