Next: Creative mathematics Up: Mathematical structure Previous: Gödel's Incompleteness Theorem   Contents

# The Halting Problem

We begin with some notation.

1. A computer program with a single integer parameter and a single integer output is represented by . is the Gödel number of the program. is the parameter. is the integer output.
2. If halts we write .
3. We only consider programs with an output when they halt that is either 1 or 0. If then or .

Now we can give a sketch of the proof of the unsolvability of the Halting Problem.

The halting problem asks does there exist a computer program such that if and if not . We give a proof by contradiction. We assume exists and prove this leads to a contradiction.

For any program with a single integer parameter it is straightforward to compute such that behaves exactly as . This says for a given program and parameter we can compute which is the Gödel number of a program that has embedded in the program and acts like with parameter . It easy to modify to create . We reserve some block of program memory for and read that location instead of reading an input parameter.

Using the above technique we can use a solution to the halting problem to solve the halting problem for a computer program with any parameter. Such a program if halts and 0 otherwise.

Now construct a program from such that will not halt but loop forever if (equivalent to ) and otherwise it will halt.

must have some Gödel number . What does do? is the same as . If halts then is designed to run forever! Therefore , and cannot exist.

This sketch of a proof is far simpler than Gödel's result. The program modifications we describe 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.)