4 ms·

>The belief that Church defined computation rigorously when he solved the Entschidungsproblem using the lambda calculus rather than just made an imprecise conje

• pron 10y ago
  You're free to believe what you want, or you can go read the abundant material, starting with Church's paper. If you find a thorough treatment of the concept of computation, you can write a paper about it. Church himself explicitly writes that he's unable to give a precise definition. Church was the first (scooping Turing by a few months) to claim that a certain formalism is what we now call Turing complete, i.e., universal with respect to the "vague intuitive notion" of the algorithm, but he was unable to provide a satisfactory justification for his claim (he made a circular argument and then gave up, writing the sentence I quoted above). Turing, on the other hand, gives a fundamental treatment of what computation is, independent of any particular formalism (in his review of Turing's paper, Church described it as explaining how to construct "arbitrary" computing systems, and Gödel said, in the quote I've given, that Turing was able to give a general, universal, treatment of what a formal system is). While I can't argue with your claim that Turing had worked with lambda calculus prior to writing On Computable Numbers when he was 24, I have seen no mention of this, but would be happy to see a reference.