That's true. The part that "feels" weird is that there is no algorithm that could perform the separation into halting / non-halting subsets. Choosing elements f

That's true. The part that "feels" weird is that there is no algorithm that could perform the separation into halting / non-halting subsets. Choosing elements from a set based on uncomputable properties almost feels like an extension of the axiom of choice.