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 Observe that in fact Peano's axioms are 9 in number and axiom 9 is the recursion/induction axiom.

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]". Because of this, "the consistency of P is unprovable in P, provided P is consistent". 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: 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 dissertation proved that Frege's rules were complete "... in the sense that every valid formula is provable". 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". 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"?) 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:

Simple arithmetic functions irreducible to primitive recursion

Gabriel Sudan (1927) and Wilhelm Ackermann (1928) display recursive functions that are not primitive recursive: In subsequent years Kleene 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: Kleene concludes 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, 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 Systems I. In his preface to this paper Martin Davis delivers a caution:

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 Davis Davis observes that Dawson states that these lectures were meant to clarify concerns that the "incompleteness theorems were somehow dependent on the particularities of formalization":

Gödel's Lectures at Princeton

Kleene and Rosser transcribed Gödel's 1934 lectures in Princeton. In his paper General Recursive Functions of Natural Numbers Kleene states:

Church definition of "effectively calculable"

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. Another footnote, 9, is also of interest. 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": 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". In Church (1936) we see, under the chapter §7 The notion of effective calculability, a footnote 18 which states the following: By "identifying" Church means – not "establishing the identity of" – but rather "to cause to be or become identical", "to conceive as united" (as in spirit, outlook or principle) (vt form), and (vi form) as "to be or become the same".

Post and "effective calculability" as "natural law"

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" performing machine-like "primitive acts" on a sheet of paper in each box. The worker is equipped with "a fixed unalterable set of directions". Each instruction consists of three or four symbols: (1) an identifying label/number, (2) an operation, (3) next instruction ji; however, if the instruction is of type (e) and the determination is "yes" THEN instruction ji' ELSE if it is "no" instruction ji. The "primitive acts" are of only 1 of 5 types: (a) mark the paper in the box he's in (or over-mark a mark already there), (b) erase the mark (or over-erase), (c) move one room to the right, (d) move one room to the left, (e) determine if the paper is marked or blank. The worker starts at step 1 in the starting-room, and does what the instructions instruct them to do. (See more at Post–Turing machine.) This matter, mentioned in the introduction about "intuitive theories" caused Post to take a potent poke at Church: In other words Post is saying "Just because you defined it so doesn't make it truly so; your definition is based on no more than an intuition." Post was searching for more than a definition: "The success of the above program would, for us, change this hypothesis not so much to a definition or to an axiom but to a natural law. 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." This contentious stance finds grumpy expression in Alan Turing 1939, and it will reappear with Gödel, Gandy, and Sieg.

Turing and computability

A. M. Turing's paper On Computable Numbers, With an Application to the Entscheidungsproblem was delivered to the London Mathematical Society in November 1936. Again the reader must bear in mind a caution: as used by Turing, the word "computer" is a human being, and the action of a "computer" he calls "computing"; for example, he states "Computing is normally done by writing certain symbols on paper" (p. 135). But he uses the word "computation" in the context of his machine-definition, and his definition of "computable" numbers is as follows: What is Turing's definition of his "machine?" Turing gives two definitions, the first a summary in §1 Computing machines and another very similar in §9.I derived from his more detailed analysis of the actions a human "computer". With regards to his definition §1 he says that "justification lies in the fact that the human memory is necessarily limited", and he concludes §1 with the bald assertion of his proposed machine with his use of the word "all" The emphasis of the word one in the above brackets is intentional. With regards to §9.I he allows the machine to examine more squares; it is this more-square sort of behavior that he claims typifies the actions of a computer (person): Turing goes on to define a "computing machine" in §2 is (i) "a-machine" ("automatic machine") as defined in §1 with the added restriction (ii): (ii) It prints two kinds of symbols – figures 0 and 1 – and other symbols. The figures 0 and 1 will represent "the sequence computed by the machine". 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. Moreover a careful reading of Turing's definitions leads the reader to observe that Turing was asserting that the "operations" of his proposed machine in §1 are sufficient to compute any computable number, and the machine that imitates the action of a human "computer" as presented in §9.I is a variety of this proposed machine. This point will be reiterated by Turing in 1939.

Turing identifies effective calculability with machine computation

Alan Turing's massive Princeton PhD thesis (under Alonzo Church) appears as Systems of Logic Based on Ordinals. In it he summarizes the quest for a definition of "effectively calculable". He proposes a definition as shown in the boldface type that specifically identifies (renders identical) the notions of "machine computation" and "effectively calculable". This is a powerful expression. because "identicality" is actually an unequivocal statement of necessary and sufficient conditions, in other words there are no other contingencies to the identification" except what interpretation is given to the words "function", "machine", "computable", and "effectively calculable":

Rosser: recursion, λ-calculus, and Turing-machine computation identity

J. B. Rosser's paper An Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem states the following:

Kleene and Thesis I

Kleene defines "general recursive" functions and "partial recursive functions" in his paper Recursive Predicates and Quantifiers. The representing function, mu-operator, etc make their appearance. He goes on in §12 Algorithm theories to state his famous Thesis I, what he would come to call Church's Thesis in 1952:

Kleene's Church, Turing, and Church–Turing theses

In his chapter §60, Kleene defines the "Church's thesis" as follows: On page 317 he explicitly calls the above thesis "Church's thesis": About Turing's "formulation", Kleene says: Kleene proposes that what Turing showed: "Turing's computable functions (1936-1937) are those which can be computed by a machine of a kind which is designed, according to his analysis, to reproduce all the sorts of operations which a human computer could perform, working according to preassigned instructions." Kleene defines Turing's Thesis as follows: Indeed immediately before this statement, Kleene states the Theorem XXX:

Gödel, Turing machines, and effectively calculability

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, 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). This was in a letter to Martin Davis (presumably as he was assembling The Undecidable). 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. So, despite appearances to the contrary, footnote 3 of these lectures is not a statement of Church's thesis."

Gandy: "machine computation", discrete, deterministic, and limited to "local causation" by light speed

Robin Gandy's influential paper titled Church's Thesis and Principles for Mechanisms appears in Barwise et al. Gandy starts off with an unlikely expression of Church's Thesis, framed as follows: Robert Soare (1995, see below) had issues with this framing, considering Church's paper (1936) published prior to Turing's "Appendix proof" (1937). Gandy attempts to "analyze mechanical processes and so to provide arguments for the following: Gandy "exclude[s] from consideration devices which are essentially analogue machines ... .The only physical presuppositions made about mechanical devices (Cf Principle IV below) are that there is a lower bound on the linear dimensions of every atomic part of the device and that there is an upper bound (the velocity of light) on the speed of propagation of change". But then he restricts his machines even more: He in fact makes an argument for this "Thesis M" that he calls his "Theorem", the most important "Principle" of which is "Principle IV: Principle of local causation": In 1985 the "Thesis M" was adapted for Quantum Turing machine, resulting in a Church–Turing–Deutsch principle.

Soare

Soare's thorough examination of Computability and Recursion appears. He quotes Gödel's 1964 opinion (above) with respect to the "much less suitable" definition of computability, and goes on to add: Soare's footnote 7 (1995) also catches Gandy's "confusion", but apparently it continues into Gandy (1988). This confusion represents a serious error of research and/or thought and remains a cloud hovering over his whole program:

Breger and problem of tacit axioms

Breger points out a problem when one is approaching a notion "axiomatically", that is, an "axiomatic system" may have imbedded in it one or more tacit axioms that are unspoken when the axiom-set is presented. For example, an active agent with knowledge (and capability) may be a (potential) fundamental axiom in any axiomatic system: "the know-how of a human being is necessary – a know-how which is not formalized in the axioms. ¶ ... Mathematics as a purely formal system of symbols without a human being possessing the know-how with the symbols is impossible ..." He quotes Hilbert: Breger further supports his argument with examples from Giuseppe Veronese (1891) and Hermann Weyl (1930-1). He goes on to discuss the problem of then expression of an axiom-set in a particular language: i.e. a language known by the agent, e.g. German. See more about this at Algorithm characterizations, in particular Searle's opinion that outside any computation there must be an observer that gives meaning to the symbols used.

Sieg and axiomatic definitions

At the "Feferfest" – Solomon Feferman's 70th birthday – Wilfried Sieg first presents a paper written two years earlier titled "Calculations By Man and Machine: Conceptual Analysis", reprinted in (Sieg et al. 2002:390–409). 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. The Feferfest paper distills the prior paper to its major points and dwells primarily on Robin Gandy's paper of 1980. Sieg extends Turing's "computability by string machine" (human "computor") as reduced to mechanism "computability by letter machine" to the parallel machines of Gandy. 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 and asserts: He claims to "step toward a more satisfactory stance ... [by] abstracting further away from particular types of configurations and operations ..." Whether the above statement is true or not is left to the reader to ponder. Sieg goes on to describe Gandy's analysis (see above 1980). In doing so he attempts to formalize what he calls "Gandy machines" (with a detailed analysis in an Appendix). About the Gandy machines: