The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is n

The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is no system in which things need proving. Instead, the analogous thing is that, for any program that returns one of “halts”, “doesn’t halt”, or “unknown” and only returns the first two in cases where those are correct, there are other machines which also do that, but where they answer “unknown” for a smaller set of inputs. (E.g. you can just augment the program by hard-coding in the correct value for some input that it previously answered “unknown” for.) Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.