It is an important topic in modern mathematical theory and computer science, particularly associated with the work of Alonzo Church and Alan Turing.
[5] While Gödel’s proof would display the tools necessary for Alonzo Church and Alan Turing to resolve the Entscheidungsproblem, he himself would not answer it.
Gödel’s doctoral dissertation[7] proved that Frege's rules were complete "... in the sense that every valid formula is provable".
Subsequently in 1931 Gödel published his famous paper On Formally Undecidable Propositions of Principia Mathematica and Related Systems I.
In his paper General Recursive Functions of Natural Numbers[25] Kleene states: Church's paper An Unsolvable Problem of Elementary Number Theory (1936) proved that the Entscheidungsproblem was undecidable within the λ-calculus and Gödel-Herbrand's general recursion; moreover Church cites two theorems of Kleene's that proved that the functions defined in the λ-calculus are identical to the functions defined by general recursion: The paper opens with a very long footnote, 3.
Martin Davis states that "This paper is principally important for its explicit statement (since known as Church's thesis) that the functions which can be computed by a finite algorithm are precisely the recursive functions, and for the consequence that an explicit unsolvable problem can be given":[28] Footnote 9 is in section §4 Recursive functions: Some time prior to Church's paper An Unsolvable Problem of Elementary Number Theory (1936) a dialog occurred between Gödel and Church as to whether or not λ-definability was sufficient for the definition of the notion of "algorithm" and "effective calculability".
[32] Post's doubts as to whether or not recursion was an adequate definition of "effective calculability", plus the publishing of Church's paper, encouraged him in the fall of 1936 to propose a "formulation" with "psychological fidelity": A worker moves through "a sequence of spaces or boxes"[33] performing machine-like "primitive acts" on a sheet of paper in each box.
Only so, it seems to the writer, can Gödel's theorem ... and Church's results ... be transformed into conclusions concerning all symbolic logics and all methods of solvability.
"[35] This contentious stance finds grumpy expression in Alan Turing 1939, and it will reappear with Gödel, Gandy, and Sieg.
A. M. Turing's paper On Computable Numbers, With an Application to the Entscheidungsproblem was delivered to the London Mathematical Society in November 1936.
[36] Furthermore, to define the if the number is to be considered "computable", the machine must print an infinite number of 0's and 1's; if not it is considered to be "circular"; otherwise it is considered to be "circle-free": Although he doesn't call it his "thesis", Turing proposes a proof that his "computability" is equivalent to Church's "effective calculability": The Appendix: Computability and effective calculability begins in the following manner; observe that he does not mention recursion here, and in fact his proof-sketch has his machine munch strings of symbols in the λ-calculus and the calculus munch "complete configurations" of his machine, and nowhere is recursion mentioned.
The proof of the equivalence of machine-computability and recursion must wait for Kleene 1943 and 1952: Gandy (1960) seems to confuse this bold proof-sketch with Church's Thesis; see 1960 and 1995 below.
Alan Turing's massive Princeton PhD thesis (under Alonzo Church) appears as Systems of Logic Based on Ordinals.
He proposes a definition as shown in the boldface type that specifically identifies (renders identical) the notions of "machine computation" and "effectively calculable".
"[53] Kleene defines Turing's Thesis as follows: Indeed immediately before this statement, Kleene states the Theorem XXX: To his 1931 paper On Formally Undecidable Propositions, Gödel added a Note added 28 August 1963 which clarifies his opinion of the alternative forms/expression of "a formal system".
He reiterates his opinions even more clearly in 1964 (see below): Gödel 1964 – In Gödel's Postscriptum to his lecture's notes of 1934 at the IAS at Princeton,[55] he repeats, but reiterates in even more bold terms, his less-than-glowing opinion about the efficacy of computability as defined by Church's λ-definability and recursion (we have to infer that both are denigrated because of his use of the plural "definitions" in the following).
The repeat of some of the phrasing is striking: Footnote 3 is in the body of the 1934 lecture notes: Davis does observe that "in fact the equivalence between his [Gödel's] definition [of recursion] and Kleene's [1936] is not quite trivial.
Earlier Sieg published "Mechanical Procedures and Mathematical Experience" (in George 1994, p. 71ff) presenting a history of "calculability" beginning with Richard Dedekind and ending in the 1950s with the later papers of Alan Turing and Stephen Cole Kleene.
Sieg cites more recent work including "Kolmogorov and Uspensky's work on algorithms" and (De Pisapia 2000), in particular, the KU-pointer machine-model), and artificial neural networks[72] and asserts: He claims to "step toward a more satisfactory stance ... [by] abstracting further away from particular types of configurations and operations ..."[72] Whether the above statement is true or not is left to the reader to ponder.