Why does the unsolvability of the Halting Problem give a negative solution to the decision problem

decidability

So Hilbert famously asked for a formalization of all of mathematics which was computationally decidable. Gödel is credited with shattering the idea that "all of mathematics" can be formalized. After all, one can't even formalize all of elementary arithmetic. But the decision problem (Entscheidungsproblem) was still considered open until Church/Turing.

I've read a fair number of popular accounts of this period. They always end with "finally the unsolvability of the Halting Problem completely shattered Hilbert's dream" and no further explanation. I feel like there are a few steps missing here. Why exactly does the unsolvability of the Halting Problem go against the decision problem?

Presumably the argument is: a formalization of all of mathematics has to be able to formalize Turing machines. Hence, it contains sentences of the form "Turing machine T halts". A decision procedure for such a formal system would therefore solve the Halting Problem. And that can't be done.

But Turing machines were a very new invention at the time. Why didn't people try to rescue the decision problem by saying Turing machines weren't an objective for formalization? And why does nobody seem to feel obligated to show that the decision problem can't be solved regardless?

Best Answer

Even assuming we're okay drastically restricting the scope of mathematics to be decided - which flies in the face of the whole idea of the program - there's still a fundamnetal issue: the arithmetizability of computation. Basically, in order to rescue decidability you'd have to restrict all the way down to triviality.

This is a riff on Godel's incompleteness theorem. Just as with GIT we used arithmetic to talk about proofs, we can talk about Turing machines in the language of arithmetic. (I don't know when this was first explicitly stated, but it's pretty much immediate once Godel's ideas are understood - certainly Kleene's $T$-predicate, which appeared only seven years after Turing's paper, does the job.) The point is that from a computable solution to the Entscheidungsproblem we can construct a computable consistent completion of PA (just go through sentences one by one with a consistency-preserving greedy algorithm), but by the arithmetization of computation (plus Rosser's improvement of GIT as originally stated) Godel's incompleteness theorem applies to any computably axiomatizable consistent extension of PA.

Indeed, looking a bit closer we get that even the $\Sigma_1$ fragment of the consequences of PA is not computable. Since the $\Delta_0$ fragment (= bounded quantifiers only) is trivially computable, this says that incompleteness hits arithmetic as hard as it possibly could. And at this point there's really nothing left to do.

Combining all this with the fact that restricting the scope goes against the whole spirit of the program to begin with, I think that explains why the conclusion was (and is) pretty universal. Note that the study of decidable fragments of arithmetic is definitely alive and well, it's just recognized as a fundamentally different thing than Hilbert's program.

Related Question