﻿AI Blue Dot | The formal definition of algorithm

# 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.