# Halting problem confusion

Does the non-solvability of the halting problem mean that no program can tell if an arbitrary program halts, or only that if such a program exists then there is no computable proof that it works?

-
Didn't know you were into computers, Jesus... –  The Chaz 2.0 May 31 '12 at 14:33
The first. There is no program such that $\dots$ –  André Nicolas May 31 '12 at 14:33

A program that decides it (and works correctly for all input programs) cannot exist at all.

Or in other words, every program can be proven not to answer the halting problem correctly. Given a purported halting solver we can construct, through a diagonalization argument, an input program that the purported solver will give the wrong answer on.

-
Ok, but by 'proven' here, you mean in a formal system? And the diagonlization proof takes place within this formal system itself? Or do we need another formal system to diagonlize over it? –  user1708 May 31 '12 at 14:40
Yes, in any formal system where you can define what it means to run a program in the first place -- plus some very mild conditions to ensure that you can formalize manipulation of programs texts in a meaningful way. There is no metamathematics involved. –  Henning Makholm May 31 '12 at 14:47

It means the former: there is no program $e$ that computes the characteristic function of the set $K = \{ i : \text{program } i \text{ halts on input } i\}$. Undecidablity has nothing to do with provable computability, it it just about actual computability.

-