Does the halting problem imply the existence of a program whose halting is independent of any formal system?

The undecidability of the halting set is done via proof by contradiction (in the constructively friendly way), i.e. we assume there exists some algorithm by we can determine whether an arbitrary program halts and we show that that leads to a contradiction, so we say no such program exists. But can we then conclude that for any formal system there exist programs which we cannot prove they will halt and we cannot prove they will not halt? There seems to be some connection to Godel's 1st Incompleteness Theorem here. The question also arises in relation to the Collatz conjecture. It was proved that an appropriate generalization can be constructed for which the Collatz conjecture is generally undecidable, but does that mean it is possible that we could prove the Collatz conjecture independent of ZF (or ZFC). That seems ridiculous, as the Collatz conjecture is the sort of computational claim that one would expect is either true or false, not undecidable.

• Yes, this a consequence of incompleteness and a way to prove it. Take a look at those kind of things – reuns Oct 12 '18 at 3:09