The history of the Church–Turing thesis ("thesis") involves the history of the development of the study of the nature of functions whose values are effectively calculable; or, in more modern terms, functions whose values are algorithmically computable. It is an important topic in modern mathematical theory and computer science, particularly associated with the work of Alonzo Church and Alan Turing.
The debate and discovery of the meaning of "computation" and "recursion" has been long and contentious. This article provides detail of that debate and discovery from Peano's axioms in 1889 through recent discussion of the meaning of "axiom".
Peano's nine axioms of arithmetic In 1889, Giuseppe Peano presented his The principles of arithmetic, presented by a new method, based on the work of Dedekind. Soare proposes that the origination of "primitive recursion" began formally with the axioms of Peano, although "Well before the nineteenth century mathematicians used the principle of defining a function by induction. Dedekind 1888 proved, using accepted axioms, that such a definition defines a unique function, and he applied it to the definition of the functions m+n, m x n, and mn. Based on this work of Dedekind, Peano 1889 and 1891 wrote the familiar five [sic] axioms for the positive integers. As a companion to his fifth [sic] axiom, mathematical induction, Peano used definition by induction, which has been called primitive recursion (since Péter 1934 and Kleene 1936) ... ."Soare 1996:5
Observe that in fact Peano's axioms are 9 in number and axiom 9 is the recursion/induction axiom.cf: van Heijenoort 1976:94
"Subsequently the 9 were reduced to 5 as "Axioms 2, 3, 4 and 5 which deal with identity, belong to the underlying logic. This leaves the five axioms that have become universally known as "the Peano axioms ... Peano acknowledges (1891b, p. 93) that his axioms come from Dedekind ... ."van Heijenoort 1976:83
Hilbert and the At the International Congress of Mathematicians (ICM) in 1900 in Paris the famous mathematician David Hilbert posed a set of problems – now known as Hilbert's problems – his beacon illuminating the way for mathematicians of the twentieth century. Hilbert's 2nd and 10th problems introduced the (the "decision problem"). In his 2nd problem he asked for a proof that "arithmetic" is "consistent". Kurt Gödel would prove in 1931 that, within what he called "P" (nowadays called Peano Arithmetic), "there exist undecidable sentences [propositions]".Gödel 1931a in (Davis 1965:6), 1930 in (van Heijenoort 1967:596) Because of this, "the consistency of P is unprovable in P, provided P is consistent".Gödel’s theorem IX, Gödel 1931a in (Davis 1965:36) While Gödel’s proof would display the tools necessary for Alonzo Church and Alan Turing to resolve the , he himself would not answer it.
It is within Hilbert's 10th problem where the question of an actually appears. The heart of matter was the following question: "What do we mean when we say that a function is 'effectively calculable'"? The answer would be something to this effect: "When the function is calculated by a mechanical procedure (process, method)." Although stated easily nowadays, the question (and answer) would float about for almost 30 years before it was framed precisely.
Hilbert's original description of problem 10 begins as follows: "10. Determination of the solvability of a Diophantine equation. Given a Diophantine equation with any number of unknown quantities and with rational integral coefficients: To devise a process according to which it can be determined in a finite number of operations whether the equation is solvable in rational integers.This translation, and the original text in German, appears in (Dershowitz and Gurevich 2007:1-2)"
By 1922, the specific question of an applied to Diophantine equations had developed into the more general question about a "decision method" for any mathematical formula. Martin Davis explains it this way: Suppose we are given a "calculational procedure" that consists of (1) a set of axioms and (2) a logical conclusion written in first-order logic, that is—written in what Davis calls "Frege's rules of deduction" (or the modern equivalent of Boolean logic). Gödel’s doctoral dissertationGödel 1930 in (van Heijenoort 1967:592ff) proved that Frege's rules were complete "... in the sense that every valid formula is provable".van Heijenoort 1967:582 Given that encouraging fact, could there be a generalized "calculational procedure" that would tell us whether a conclusion can be derived from its premises? Davis calls such calculational procedures "algorithms". The would be an algorithm as well. "In principle, an algorithm for [the] would have reduced all human deductive reasoning to brute calculation".Davis 2000:146
In other words: Is there an "algorithm" that can tell us if any formula is "true" (i.e. an algorithm that always correctly yields a judgment "truth" or "falsehood"?) " ... it seemed clear to Hilbert that with the solution of this problem, the Entscheidungsproblem, that it should be possible in principle to settle all mathematical questions in a purely mechanical manner. Hence, given unsolvable problems at all, if Hilbert was correct, then the Entscheidungsproblem itself should be unsolvable".Davis 1965:108
Indeed: What about our algorithm itself? Can it determine, in a finite number of steps, whether it, itself, is "successful" and "truthful" (that is, it does not get hung up in an endless "circle" or "loop", and it correctly yields a judgment "truth" or "falsehood" about its own behavior and results)?
Three problems from Hilbert's 2nd and 10th problems At the 1928 Congress [in Bologna, Italy] Hilbert refines the question very carefully into three parts. The following is Stephen Hawking's summary: "1. To prove that all true mathematical statements could be proven, that is, the completeness of mathematics. "2. To prove that only true mathematical statements could be proven, that is, the consistency of mathematics, "3. To prove the decidability of mathematics, that is, the existence of a decision procedure to decide the truth or falsity of any given mathematical proposition."Hawking 2005:1121
Simple arithmetic functions irreducible to primitive recursion Gabriel Sudan (1927) and Wilhelm Ackermann (1928) display recursive functions that are not primitive recursive:
"Are there recursions that are not reducible to primitive recursion; and in particular can recursion be used to define a function which is not primitive recursive?
"This question arose from a conjecture of Hilbert in 1926 on the continuum problem, and was answered [yes: there are recursions that are not primitive recursive] by Ackermann 1928."Kleene 1952:271
In subsequent years Kleenecf. Kleene 1952:272-273 observes that Rózsa Péter (1935) simplified Ackermann's example ("cf. also Hilbert-Bernays 1934") and Raphael Robinson (1948). Péter exhibited another example (1935) that employed Cantor's diagonal argument. Péter (1950) and Ackermann (1940) also displayed "transfinite recursions", and this led Kleene to wonder: "... whether we can characterize in any exact way the notion of any "recursion", or the class of all "recursive functions."Kleene 1952:273
Kleene concludescf. Kleene 1952:274 that all "recursions" involve (i) the formal analysis he presents in his §54 Formal calculations of primitive recursive functions and, (ii) the use of mathematical induction. He immediately goes on to state that indeed the Gödel-Herbrand definition does indeed "characterize all recursive functions" – see the quote in 1934, below.
Gödel's proof In 1930, mathematicians gathered for a mathematics meeting and retirement event for Hilbert. As luck would have it, "at the very same meeting, a young Czech mathematician, Kurt Gödel, announced results which dealt it [Hilbert's opinion that all three answers were YES] a serious blow."Hodges 1983:92
He announced that the answer to the first two of Hilbert's three questions of 1928 was NO.
Subsequently in 1931 Gödel published his famous paper On Formally Undecidable Propositions of Principia Mathematica and Related In his preface to this paper Martin Davis delivers a caution: "The reader should be warned that [in this particular paper] what Gödel calls recursive functions are now called primitive recursive functions. (The revised terminology was introduced by KleeneKleene 1936 in (Davis 1965:237ff))."Davis 1965:4
Gödel expansion of "effective calculation" To quote Kleene (1952), "The characterization of all "recursive functions" was accomplished in the definition of 'general recursive function' by Gödel 1934, who built on a suggestion of Herbrand" (Kleene 1952:274). Gödel delivered a series of lectures at the Institute for Advanced Study (IAS), Princeton NJ. In a preface written by Martin DavisDavis 1965:39–40 Davis observes that "Dr. Gödel has stated in a letter that he was, at the time of these lectures, not at all convinced that his concept of recursion comprised all possible recursions ..."Davis 1965:40
Dawson states that these lectures were meant to clarify concerns that the "incompleteness theorems were somehow dependent on the particularities of formalization":(Dawson 1997:101)
"Gödel mentioned Ackermann's example in the final section of his 1934 paper, as a way of motivating the concept of "general recursive function" that he defined there; but earlier in footnote 3, he had already conjectured (as "a heuristic principle") that all finitarily computable functions could be obtained through recursions of such more general sorts.
"The conjecture has since elicited much comment. In particular, when Martin Davis undertook to publish Gödel's 1934 lectures [in Davis 1965:41ff] he took it to be a variant of Church's Thesis; but in a letter to Davis ...[246: "KG to Martin Davis, 15 February 1965, Quoted in Gödel 1986–, vol. I, p. 341"] Gödel stated emphatically that that was "not true" because at the time of those lectures he was "not at all convinced" that his concept of recursion comprised "all possible recursions." Rather, he said, "The conjecture stated there only refers to the equivalence of 'finite (computation) procedure' and 'recursive procedure.'" To clarify the issue Gödel added a postscript to the lectures,Gödel 1964 in (Davis 1965:247) also reprinted in (Gödel 1986, vol. I:369–371) in which he indicated that what had finally convinced him that the intuitively computable functions coincided with those that were general recursive was Alan Turing's work . "Gödel's reluctance to regard either general recursiveness or λ-definability as adequate characterization of the informal notion of effective computability has been examined in detail by several authors [Footnote 248: "See especially Davis 1982; Gandy 1980 and 1988; Sieg 1994"]. There is a consensus that, in fact, neither Gödel's nor Church's formalisms were so perspicuous or intrinsically persuasive as Alan Turing's analysis, and Wilfried Sieg has argued that the evidence in favor of Church's Thesis provided by the "confluence of different notions" (the fact that the systems proposed by Church, Gödel, Post and Alan Turing all turned out to have the same extension) is less compelling than has generally supposed. Hence, quite apart from Gödel's innate caution there were good reasons for his skepticism. But what, then, was he attempting to achieve through his notion of general recursiveness? ...