The paper “On computable numbers, with an application to the Entscheidungsproblem” by Alan Turing was published in 1936 and in addition to having a really cool title is a cornerstone piece of computational theory. Before we get to the paper, though, first we need to go over a a bit of background.
The Entscheidungsproblem was proposed by David Hilbert in 1928.
Hilbert asked if it was possible to create an algorithm that would take as input a statement in a formal language and answer whether that statement was true or false. In other words the algorithm would provide an answer as to the decidability of the inputted statement. Entscheidungs is German for decision and Hilbert was German himself, and so entscheidungsproblem was the term given to his question. This was all in parallel and partly in response to Russell and Whitehead’s work on the Principia Mathematica in the earlier part of the century. It appears that Hilbert believed that the answer to his question would be yes and set about trying to create a foundational system that would meet his requirements. This effort in mathematics was known as the Hilbert Programme.
The main goal of Hilbert’s program was to provide secure provable foundations for all of mathematics. Hilbert proposed the creation of a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert then further proposed that the consistency of more complicated systems could be proven in terms of these simpler systems. The basic steps for doing this would include:
- There would need to be formalization system for all of mathematics. Every mathematical statements should be able to be written in this formal language. This formal language would need to be able to be manipulated according to well defined rules. (No step such as–“and then something magic happens.”)
- Completeness: There would need to be a proof that all true mathematical statements can be proven in the formal system.
- Consistency: The formal system would need to be consistent with itself. This means that there would need to be a proof that no contradiction can be obtained in the formal system of mathematics.
- Conservation: There would need to be a proof that any result about “real objects” obtained using reasoning about “ideal objects” (such as uncountable sets) can be proven without having to use ideal objects to obtain the proof.
- Decidability: This gets to the well established rules. To satisfy this requirement there should be an algorithm for deciding the truth or falsity of any mathematical statement within the formal system.
In 1931, Kurt Gödel produced the paper “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I”, Monatshefte für Mathematik und Physik, 38: 173–198. Here’s a link to an english translation–On formally undecidable propositions of Principia
Mathematica and related systems. This is another truly amazing paper and I may do a whole post about it sometime. For now, lets just summarize and say that it deals with points 1 – 4 above. Basically, Gödel showed that in any system of mathematics sufficiently powerful to describe itself it was possible to create propositions that were inherently contradictory. The propositions may be thought of as being of the form “This statement is false.” In particular, Gödel used a very clever technique to encode propositions in a formal language into numbers. These numbers are called Gödel numbers. Gödel didn’t, however, say anything about the decidability question. That (finally) brings us to Turing in 1936.
Continue reading On “On computable numbers, with an application to the Entscheidungsproblem”