PDF version of this book

The Halting Problem

Following is some needed notation.

1. A computer program with no inputs is represented by $t_n$ where $n$ is the Gödel number of the program.

2. A computer program with a single integer parameter is represented by $p_n(m)$. $n$ is the Gödel number of the program. $m$ is the parameter. If a program halts it may generate an output value. This is written as $V(t_n)$ and $V(p_n(m)$.

3. If $t_n$ or $p_n(m)$ halts, write $H(t_n)$ or $H(p_n(m))$ respectively.

Following is a sketch of the proof of the unsolvability of the Halting Problem.

The Halting Problem asks does there exist a computer program $h(n)$ such that $V(h(n))=1$ if $H(t_n)$ and $V(h(n)) = 0$ otherwise.

Assume $h(n)$ exists. The following shows that this leads to a contradiction.

From $h(n)$ one can construct $s(n)$ (for the Self Halting Problem). $V(s(n)) = 1$ if $p_n(n)$ halts. otherwise it equals 0. In other words $s(n)$ decides whether any computer program that accepts a single integer parameter as input will halt when presented with its own Gödel number as input.

For any program $p_n$ it is straightforward to compute $k$ such that $t_k$ behaves exactly as $p_n(n)$. To construct $t_k$ from $p_n$ expand the program memory to include the value $n$ and read that data instead of reading an input parameter. Thus from a solution to the Halting Problem one can construct a solution to the Self Halting Problem.

Now $s$, which solves the Self Halting Problem, is a computer program that accepts an integer input, Thus it has a Gödel number $r$ and $p_r(n)$ is identical to $s(n)$. From $r$ one can construct a program with Gödel number $q$ such that $p_q(n)$ halts if $V(s(n)) = 0$, otherwise it runs forever.

What does $p_q(q)$ do? If $p_q(q)$ halts then $V(s(q)) = 1$ and thus $p_q(q)$ will run forever. This is a contradiction and thus the original assumption that $h(n)$, a solution to the Halting Problem, exists is false.

This sketch of a proof is far simpler than Gödel's result. The program modifications described are straight forward for an experience programmer, but the details at the level of computer code are tedious. It is even more tedious to prove the modifications do what is intended. Gödel's proof in 1931 never mentioned computers. He went through the long and difficult exercise of showing that a formal system could be modeled as an arithmetic function definable within the formal system. He then proved the consistency of the formal system was equivalent to a question about this function. Using an argument similar to the above he showed one could not prove that property from within the system unless the system itself was inconsistent. One can prove anything in an inconsistent system.

PDF version of this book