  A few years later, Church and Turing independently proved that the entscheidungsproblem is unsolvable. Church did this by using the methods of Gödel’s Incompleteness Theorem to show that the set of satisfiable formulas of first-order logic is not r.e., i.e., they cannot be systematically listed out by a function computable by the lambda calculus. Turing introduced his machines and proved many interesting theorems some of which we will discuss in the next section. In particular, he proved the unsolvability of the halting problem. He obtained the unsolvability of the entscheidungsproblem as a corollary.