Computation

Original: 02/01/20
Revised: no

As part of his quest to put the foundations of mathematics on solid footing, in 1928 Hilbert also asked for an algorithm which would take a statement in FOL and decide whether that statement was provable or not, known as Entscheidungsproblem, which is "the decision problem" in German. The problem triggered a search for an agreed upon definition of what an algorithms is. Many candidates were proposed in the years following Hilbert's call, among them Alonzo Church's Lambda Calculus, Gödel's Recursive Functions, Emil Post's Production Systems and Alan Turing's Turing Machines. In short order, J.B Rosser showed that all these candidates were equivalent in power, and that equivalence strengthened the belief that the informal notion of an algorithm had been captured formally. Intuitively, the Turing machine was the most convincing candidate, and Gödel himself (who invented one of the equivalent mechanisms, the recursive functions) was persuaded that the notion of algorithm had been captured only because of the Turing machine formalism. The thesis that these equivalent formulations have formally captured the informal notion of an algorithm, namely an effective mechanical procedure to be carried out in precise steps, is called the Church-Turing thesis; the term was coined by Stephen Kleene, whose work was instrumental in clarifying much of the work involving those equivalences. It is the now the fundamental assumption behind computation.

In 1935, Alan Turing published his most famous paper: "On Computable Numbers, With an Application to the Entscheidungsproblem" and gave a negative answer to Hilbert's Entscheidungsproblem: there is no algorithm that would decide whether a statement in FOL is provable or not. Turing reduced the Entscheidungsproblem to the Halting Problem, which is described in the video below. You will also see in the video that Turing's proof of the undecidability of the Halting Problem uses an idea which is similar with Gödel's idea in his proofs. While Gödel carefully built a statement \(G_1\) to assert its own unprovability, Turing built a Turing machine which would be fed as an input to itself. Here is the description of Turing's proof that the Halting problem is undecidable:

So you would probably suspect now that the two concepts of undecidability, the undecidability in Gödel's theorems and the Turing undecidability shown above, although different concepts, are very much related, because we have seen that the incompleteness theorems and the halting problem are about similar impossibilities. And indeed, one can give a very simple proof of a weaker version of the first incompleteness theorem using Turing's result that the halting problem is undecidable. In the weaker version, consistency is replaced with soundness (terms we have defined in Formal Systems), but the main ideas are fully captured. And from our point of view, the use of undecidability of the Halting problem to prove undecidability in the formal system \(G_1\) brings together the two concepts we need the most in our website, computation and undecidability.