Tell me more ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.
up vote 1 down vote favorite

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?

share|improve this question
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

2 Answers

up vote 6 down vote accepted

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.

share|improve this answer
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? – Holowitz May 31 '12 at 14:40
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. – Henning Makholm May 31 '12 at 14:47
up vote 3 down vote

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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