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

Question

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?

Answer 1

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.

Answer 2

There were several proofs of undecidability and incompleteness using very different tools, from Church, Post, Godel and Turing. They are all equivalent.

Godel's proof is the probably the most direct, because it used nothing more abstract than ordinary arithmetic.

Turing's may be the most consequential, because it has been used to provide a definition of "computability", which is an incredibly rich subject on its own.

Both Godel and Turing's proof depended on the idea of self-reference, where a system as a whole is represented as an object of the system. With Turing, we are talking about what happens when a program takes a program as input. With Godel, we are looking at what happens when we encode a theorem of arithmetic as an integer. You can see the parallel here and have a sense of how they are equivalent.

With Godel's proof, there is no escaping the fact that arithmetic must be either undecidable or incomplete.

If you are new to the subject, I recommend Douglas Hofstadter's classic Godel, Escher, Bach, an entertaining book that can give you tools to visualize how these proofs work.