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