Incompleteness and Halting. Gödel and Turing.
The following occurred to me on a run about two years ago:
It’s not given much press, but the the Halting Problem is intimately related to Gödel’s First Incompleteness Theorem. Indeed it produces it as a correllary. Historically, Gödel’s incompleteness results were proved by hacking arithmetic into a Turing complete system, and this is still how they’re explained today.
There’s a one-to-one bijection between computability of a function and provability of a statement. Hence, the short, and generally accessible proof that the Halting problem is not in general computable for an arbitrary input is also a proof of the ‘most important, surprising result in logic’, namely, that some results, which have may have a perfectly valid truth-value outside a system, cannot be proven within it. One only needs the notion of a computer to follow this line of thinking, which is, in essence, what Gödel did. But the Halting problem is much easier to grasp. I’ve had children understand it, though it does take some walking through!
The interesting thing about the Halting problem is that it’s unsolvable in full generality, independent of whatever special capabilities the system has available. To see this clearly, consider the proof.
Question: Does there exist a (halting) program H which, given any program P, figure out if it would halt, for any input I?
Assume there exists such a program H. Construct a program T as follows.
(Program P, Input I) => (Boolean Halts):
if H(P,I) is true run forever
otherwise halt
Now, call T on itself, with itself as an input. Our assumption presupposes that H always halts. If T would halt on input T, then T will run forever. And if T would run forever on input T, then T would halt. This is a contradiction, so no such program H would exist.
