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.

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

With suitable hypotheses, the answer to your question is "yes". The suitable hypotheses would include that the formal system is sound (in particular, if it proves that a certain computation never halts then that computation will not in fact halt) and that it's effective, i.e., that an algorithm can tell what is and what is not a proof.

Now if we had such a formal system that could prove, for any given program (and input) that it halts or that it doesn't halt, then we'd have the following decision procedure for the halting problem. To decide whether a given program halts, start running the program and, in parallel, start searching for a proof, in your formal system, that it doesn't halt. If the program halts, output "yes"; if you find a proof that it doesn't halt, then output "no".

Since there cannot be a decision algorithm for the halting problem, this argument shows that there cannot be a formal system (of the sort described above) that proves non-halting for all programs that don't in fact halt.

  • $\begingroup$ But has anyone been able to construct such a program that provably can neither be shown to halt or not to halt? Or has it just been showed that such programs will always exist in some sense? $\endgroup$ – Keefer Rowan Oct 11 '18 at 22:47
  • 1
    $\begingroup$ Given a particular formal system (satisfying the hypotheses in my answer), it is fairly straightforward to produce a program that never halts but for which that formal system can't prove that it doesn't halt. One can use the argument in my answer plus the proof of undecidability of the halting problem. Or one can use Gödel's incompleteness theorems. For example, a program that systematically searches for a contradiction in ZFC will never halt (because ZFC is consistent), but ZFC can't prove that. $\endgroup$ – Andreas Blass Oct 11 '18 at 22:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.