A Halting Oracle that only says “Yes”, “No”, or “Provably Undecidable” hasn’t (to my knowledge and research) been proven to be impossible
I think I just proved this. If you can prove something is undecidable, it creates a paradox.
nor do they demonstrate that we can’t prove that any given algorithm will or will not halt
If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases. There are some programs which do not halt, but which it’s impossible to prove they will not halt.
nor do they even demonstrate that an algorithm can’t prove that other algorithms will or will not halt
“If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases.”
That is only true if your proofs work from the same one set of axioms. But in reality you can choose different sets of axioms as needed. So it may be possible to prove of each and every algorithm that it will halt or not, but you cannot make a halt-detection machine that works in all cases, because your proofs use different sets of axioms.
I think I just proved this. If you can prove something is undecidable, it creates a paradox.
If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases. There are some programs which do not halt, but which it’s impossible to prove they will not halt.
But not for all cases, see above.
“If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases.”
That is only true if your proofs work from the same one set of axioms. But in reality you can choose different sets of axioms as needed. So it may be possible to prove of each and every algorithm that it will halt or not, but you cannot make a halt-detection machine that works in all cases, because your proofs use different sets of axioms.