= Separation of number sets in an arithmetic theory
{title2=$n\in A\Rightarrow S\vdash H(\bar n),\quad n\in B\Rightarrow S\vdash\neg H(\bar n)$}
A formula separates the number <set> $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a <consistent first-order theory>[consistent] <first-order theory>[theory] the <sets> must be disjoint. A diagonal sentence asserting the <negation> of its membership in a separator of provable from refutable codes is undecidable by the two direct <contradiction> cases.
Back to article page
