0
$\begingroup$

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?

  • 0
    The first. There **is** no program such that $\dots$2012-05-31

2 Answers 2

6

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.

  • 1
    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.2012-05-31
3

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.