> λ-calculus contributed not only to mathematics/computer science, but also, logic, linguistics, etc. Not to mention its practical contributions in many progra

> λ-calculus contributed not only to mathematics/computer science, but also, logic, linguistics, etc. Not to mention its practical contributions in many programming languages. True, but it didn't actually show what Church had wanted to show in 1936 about what later became known as computability. First, it should be clear that after Gödel's incompleteness results, it was all but certain that arithmetics was undecidable. The problem with showing that, however, was defining what a "decision procedure", or an algorithm, is. Church's approach, essentially defining it as "anything that could be expressed as a lambda expression" suffered from serious difficulties, inherent to all languages (until Turing, all discussions of computation rested on formal languages with some inference calculus), which is that the computational power of a language rests on arbitrary axioms. One could easily define a second-order lambda calculus that has an axiomatic term, H, that axiomatically reduces to whether its argument is normalizable or not, provided that it does not contain H itself. Why, then, should we choose the "first-order" lambda calculus as the definition of computation rather than the second-, third- or fourth-order? Church does a decent job explaining why "calculability" (computability) is no weaker than his lambda calculus, but his explanation for why it can't be stronger -- which is the more important point -- is poor. Church himself admits as much when he realizes his definition relies on some circularity -- as we now know, a calculus is computable iff each of its derivations are computable (which wouldn't be true for the "second-order" lambda calculus), but how can we tell that if we wish to define computability using the calculus itself? So he waves his hands a bit and then writes: [1] > If this interpretation or some similar one is not allowed, it is difficult to see how the notion of an algorithm can be given any exact meaning at all. Turing did just that. He was able to define computation in an absolute way, one that does not depend on any language or arbitrary axioms (just physical observation). As Gödel said: [2] > [W]ith this concept one has for the first time succeeded in giving an absolute definition of an interesting epistemological notion, i.e., one not depending on the formalism chosen. In all other cases treated previously, such as demonstrability or [lambda] definability, one has been able to define them only relative to a given language, and for each individual language it is clear that the one thus obtained is not the one looked for. For the concept of [Turing] computability, however, although it is merely a special kind of demonstrability or decidability, the situation is different. By a kind of miracle it is not necessary to distinguish orders, and the diagonal procedure does not lead outside the defined notion. Unlike any language, Turing's treatment has no "orders." One could, of course -- as Turing has done -- imagine a Turing machine with an oracle, but it is clear that the oracle cannot itself be a machine, while a "second-order" lambda calculus is just another language, no more or less arbitrary than the "first-order" one. The problem, then, was to define what computation was, and Turing was the first to succeed. [1]: An Unsolvable Problem of Elementary Number Theory, footnote 19 [2]: Remarks before the Princeton bicentennial conference on problems in mathematics, 1942, in Collected Works, Vol II