History of the Church-Turing thesis

This article is an extension of the history of the Church-Turing thesis.

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 1889: Peano, based on work of Dedekind, presents 9 axioms of arithmetic

Guiseppe Peano presents his "The principles of arithmetic, presented by a new method". 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 mⁿ. 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 1900: Hilbert's 2nd and 10th problems introduce the Entscheidungsproblem (the "decision problem")

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. 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 Entscheidungsproblem, he himself would not answer it.

It is within Hilbert's 10th problem where the question of an "Entscheidungsproblem" 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 "Entscheidungsproblem" 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 [Gö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 Entscheidungsproblem would be an algorithm as well. "In principle, an algorithm for [the] Entscheidungsproblem 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" algorithm 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 Entscheidungsproblem 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)?

Hilbert 1928: An expression of the three problems that derived from Hilbert's 2nd and 10th

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]

Ackermann et al. 1927-1928: Woops -- simple arithmetic functions exist that cannot be reduced to (primitive) recursion

Gabriel Sudan (1927) and Wilhelm Ackermann (1928) display recursive functions that are not "primitive" recursive:

:"Are there recursions which 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 Kleene [cf. 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 concludes [cf. 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 .

Gödel 1930-1931: Woops-- A mathematical system cannot be shown to be consistent within the system

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 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 [http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I"] . 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 Kleene [Kleene 1936 in (Davis 1965:237ff)] )." [Davis 1965:4]

Gödel 1934: Woops -- A contender for a definition "effective calculation" must be expanded from "primitive recursion" to "general" recursion"

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 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 (1937).

:"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? ...

:"Rather, Gödel obtained his definition [of the class of general recursive functions] through modification of Herbrand's ideas ...; and Wilfried Sieg has argued that his real purpose in the final section of the 1934 paper [the lecture notes] was "to disassociate recursive functions from [Herbrand's] epistemologically restricted notion of proof" by specifying "mechanical" rules for deriving equations." What was more "general" about Gödel's notion of "general" recursiveness was, Sieg suggests, that Herbrand had intended only to characterize those functions that could be "proved" to be recursive by "finitary" means [250] ." [Italics in the original Dawson 1997:101-102]

Kleene 1935

Kleene and Rosser transcribed Gödel's 1934 lectures in Princeton. In his paper "General Recursive Functions of Natural Numbers" [Kleene 1935 in (Davis 1965:236ff)] Kleene states:

:"A definition of general recursive function of natural numbers was suggested by Herbrand to Gödel, and was used by Gödel with an important modification in a series of lectures at Princeton in 1934 ... [Kleene 1935 in (Davis 1965:237)]

:"A recursive function (relation) in the sense of Gödel ... will now be called a primitive recursive function (relation). [Kleene 1935 in (Davis 1965:239)]

=Church 1936: Defines "effectively calculable" as done by (general-) recursion and the λ-calculus; not all are convinced =

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::"Theorem XVI. Every recursive function of positive integers is λ-definable.¹⁶:"Theorem XVII. Every λ-definable function of positive integers is recursive.¹⁷::"¹⁶ ... . In the form here it was first obtained by Kleene... .::"¹⁷ This result was obtained independently by the present author and S. C. Kleene at about the same time.

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" [Church 1936 in (Davis 1965:88)] :

:"³ As will appear, this definition of effective calculability can be stated in either of two equivalent forms, (1) ... λ-definable ... 2) ... recursive ... . The notion of λ-definability is due jointly to the present author and S. C. Kleene, successive steps towards it having been taken by the present author in the "Annals of Mathematics", vol. 34 (1933), p. 863, and Kleene in the "American Journal of Mathematics", vol. 57 (1935), p. 219. The notion of recursiveness in the sense of §4 below is due jointly to Jacques Herbrand and Kurt Gödel, as is there explained. And the proof of equivalence of the two notions is due chiefly to Kleene, but also partly to the present author and to J. B. Rosser ... . The proposal to identify these notions with the intuitive notion of effective calculability is first made in the present paper (but see the first footnote to §7 below).

:"With the aid of the methods of Kleene ("American Journal of Mathematics", 1935), the considerations of the present paper could, with comparatively slight modification be carried through entirely in terms of λ-definability, without making use of the notion of recursiveness. On the other hand, since the results of the present paper were obtained, it has been shown by Kleene (see his forthcoming paper, "General recursive functions of natural numbers") that analogous results can be obtained entirely in terms of recursiveness, without making use of λ-definability. The fact, however, that two such widely different and (in the opinion of the author) equally natural definitions of effective calculability turn out to be equivalent adds to the strength of the reasons adduced below for believing that they constitute as general a characterization of this notion as is consistent with the usual intuitive understanding of it." [Church 1936 in (Davis 1965:90)]

Footnote 9 is in section "§4 Recursive functions"::" ⁹This definition [of "recursive"] is closely related to, and was suggested by, a definition of recursive functions which was proposed by Kurt Gödel, in lectures at Princeton, N. J., 1934, and credited by him in part to an unpublished suggestion of Jacques Herbrand. The principal features in which present definition of recursiveness differs from Gödel's are due to S. C. Kleene.:" In a forthcoming paper by Kleene to be entitled "General recursive functions of natural numbers," ... it follows ... that every function recursive in the present sense is also recursive in the sense of Gödel (1934) and conversely." [Church 1936 in (Davis 1965:95)]

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::"¹⁸The question of the relationship between effective calculability and recursiveness (which it is here proposed to answer by identifying the two notions) was raised by Gödel in conversation with the author. The corresponding question of the relationship between effective calculability and λ-definability had previously been proposed by the author independently." [Church 1936 in (Davis 1965:100)]

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" [Merriam-Webster 1983:identifying] .

Post 1936: Church's notion of "effective calculability" was derived from inductive reasoning and therefore only expressible as a "natural law", not as a definition

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"Post 1936 in (Davis 1965:289)] performing machine-like "primitive acts" on a sheet of paper in each box. The worker is equipped with "a fixed ualterable set of directions"Post 1936 in (Davis 1965:289)] . Each instruction consists of three or four symbols: (1) an identifying label/number, (2) an operation, (3) next instruction j_i; however, if the instruction is of type (e) and the determination is "yes" THEN instruction j_i' ELSE if it is "no" instruction j_i. The "primitive acts"Post 1936 in (Davis 1965:289)] 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::"The writer expects the present formulation to turn out to be logically equivalent to recursiveness in the sense of the Gödel-Church development.⁷ Its purpose, however, is not only to present a system of a certain logical potency but also, in its restricted field, of psychological fidelity. In the latter sense wider and wider formulations are contemplated. On the other hand, our aim will be to show that all such are logically reducible to formulation 1. We offer this conclusion at the present moment as a "working hypothesis". And to our mind such is Church's identification of effective calculability with recursivness.⁸" (italics in original)::⁷ [he sketches an approach to a proof] ::⁸ "Cf. Church, lock. cit, pp. 346, 356-358. Actually the work already done by Church and others carries this identification considerably beyond the working hypothesis stage. "But to mask this identification under a definition hides the fact" that a fundamental discovery in the limitiations of mathematicizing power of Homo Sapiens has been made "and blinds us to the need of its continual verification"." [italics added, Post 1936 in (Davis 1965:291)]

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." [Italics in original, Post in (Davis 1965:291)]

This contentious stance finds grumpy expression in Alan Turing 1939, and it will reappear with Gödel, Gandy, and Sieg.

Turing 1936: Machine computation as modelled on the behavior of a (human) "computer"

A. M. Turing's paper "On Computable Numbers, With an Application to the Entscheidungsproblem" appears. 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" Turing 1937 in (Davis 1967:118)] in the context of his machine-definition, and his definition of "computable" numbers is as follows::"The "computable" numbers may be described briefly as the real numbers whose expressions as a decimal are calculable by finite means ... .According to my definition, a number is computable if its decimal can be written down by a machine." [Turing 1937 in (Davis 1967:116)]

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"Turing 1937 in (Davis 1967:117)] , and he concludes §1 with the bald assertion of his proposed machine with his use of the word "all"

:"It is my contention that these operations [write symbol on tape-square, erase symbol, shift "one" square left, shift "one" square right, scan square for symbol and change machine-configuration as a consequence of "one" scanned symbol] include all those which are used in the computation of a number."Turing 1937 in (Davis 1967:118)]

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)::"The machine scans B squares corresponding to the B squres observed by the computer. In any move the machine can change a symbol on a scanned square or can change any one of the scanned squares to another square distant not more than L squares from one of the other scanned squares ... The machines just described do not differ very essentially from computing machines as defined in §2 [sic] , and corresponding to any machine of this type a computing machine can be constructed to compute the same sequence, that is to say the sequence computed by the computer." [Turing 1937 in (Davis 1967:138)]

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".Turing 1937 in (Davis 1967:118)]

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"::"A number is computable if it differs by an integer from the number computed by a circle-free machine." [Turing 1937 in (Davis 1967:119)]

Although he doesn't call it his "thesis", Turing proposes a proof that his "computability" is equivalent to Church's "effective calculability": :"In a recent paper Alonzo Church has introduced an idea of "effective calculability", which is equivalent to my "computability", but is very differently defined ... The proof of equivalence between "computability" and "effective calculability" is outlined in an appendix to the present paper."Turing 1937 in (Davis 1967:117)]

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::"The theorem that all effectively calculable (λ-definable) sequences are computable and its converse are proved below in outline." [Turing 1937 in (Davis 1967:149)]

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 1939: "Effective calculability" is (identically) "machine computation" and vice versa

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".

:"A function is said to be "effectively calculable" if its values can be found by some purely mechanical process. Although it is fairly easy to get an intuitive grasp of this idea, it is nevertheless desirable to have some more definite, mathematically expressible definition. Such a definition was first given by Gödel at Princeton in 1934 ... . These functions are described as "general recursive" by Gödel ... . Another definition of effective calculability has been given by Church ... who identifies it with λ-definability. The author has recently suggested a definition corresponding more closely to the intuitive idea (Turing [1] , see also Post's [1] ). It was stated above that "a function is effectively calculable if its values can be found by some purely mechanical process". We may take this statement literally, understanding by a purely mechancial process one which could be carried out by a machine. It is possible to give a mathematical description, in a certain normal form, of the structures of these machines. The development of these ideas leads to the author's definition of a computable function, and to an identification of computability † with effective calculability. It is not difficult, though somewhat laborious, to prove that these three definitions are equivalent. [Kleene [3] , Turing [2] ] ::"† We shall use the expression "computable function" to mean a function calculable by a machine, and we let "effectively calculable" refer to the intuitive idea without particular identification with any one of these definitions. We do not restrict the values taken by a computable function to be natural numbers; we may for instance have computable propositional functions." [boldface added, Turing 1939 in (Davis 1965:160)]

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"::: For all functions: IF "this function is computable by machine" THEN "this function is effectively calculable" AND IF "this function is effectively calculable" THEN "this function is computable by a machine."

Rosser 1939: The first "identification" of recursion, λ-calculus and Turing-machine computation

J. B. Rosser's paper "An Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem" [Rosser 1939 in (Davis 1967:223-230)] states the following:

:"'Effective method' is here used in the rather special sense of a method each step of which is precisely predetermined and which is certain to produce the answer in a finite number of steps. With this special meaning, three different precise definitions have been given to date⁵. The simplest of these to state (due to Post and Turing) says essentially that an effective method of solving a certain set of problems exists if one can build a machine which will then solve any problem of the set with no human intervention beyond inserting the question and (later) reading the answer. All three definitions are equivalent, so it does not matter which one is used. Moreover, the fact that all three are equivalent is a very strong argument for the correctness of any one.

::⁵ One definition is given by Church in I [i.e. Church 1936 "An Unsolvable Problem of Elementary Number theory"] . Another definition is due to Jacques Herbrand and Kurt Gödel. It is stated in I, footnote 3, p. 346. The third definition was given independently in two slightly different forms by E. L. Post ... and A. M. Turing ... . The first two definitions are proved equivalent in I. The third is proved equivalent to the first two by A. M. Turing, "Computability and λ-definability" ["Journal of Symbolic Logic", vol. 2 (1937), pp. 153-163] ." [quote and footnote from Rosser 1939 in (Davis 1967:225-226)]

Kleene 1943: The first expression of "Church's Thesis" as "Thesis I" and his proposal to use it as a definition of "effectively calculable"

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:

:"This heuristic fact, as well as certain reflections on the nature of symbolic algorithmic processes, led Church to state the following thesis²². The same thesis is implicitly in Turing's description of computing machines²³.

::"Thesis I. Every effectively calculable function (effectively decidable predicate) is general recursive."

:"Since a precise mathematical definition of the term effectively calculable (effectively decidable) has been wanting, we can take this thesis, together with the principle already accepted to which it is converse, as a definition of it ... the thesis has the character of an hypothesis -- a point emphasized by Post and by Church²⁴.:::²² Church [1] ["An Unsolvable Problem of Elementary Number Theory"] [Church 1936a in (Davis 1965:88ff)] :::²³ Turing [1] ["On Computable numbers, with an application to the Entscheidungsproblem"(1937)] [Turing 1937, in (Davis 1965:115ff)] :::²⁴ Post [1, p. 105] [Post, 1936, "Finite combinatory processes - Formulation 1", The Journal of Symbolic Logic, Vol. 1, No. 3 (Sep., 1936), pp. 103-105] , and Church [2] [Church, 1938, "The constructive second number class", Bull. Amer. Math. Soc. vol. 44, Number 4, 1938, pp. 224-232] ]

Kleene 1952: The first formal expression of "Church's thesis" and "Turing's thesis" and their "identification"

In his chapter §60, Kleene defines the "Church's thesis" as follows::" ... heuristic evidence and other considerations led Church 1936 to propose the following thesis.::"Thesis I. Every effectively calculable function (effectively decidable predicate) is general recursive.:"This thesis is also implicit in the conception of a computing machine formulated by Turing 1936-7 and Post 1936." [Kleene 1952 in (Davis 1965:300-301)]

On page 317 he "explicitly" calls the above thesis "Church's thesis"::"§62. Church's thesis. One of the main objectives of this and the next chapter is to present the evidence for Church's thesis (Thesis I §60)." [Kleene 1952 in (Davis 1965:317)]

About Turing's "formulation", Kleene says::"Turing's formulation hence constitutes an independent statement of Church's thesis (in equivalent terms). Post 1936 gave a similar formulation." [Post 1936:321]

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 1952 in (Davis 1965:321)]

This interpretation of Turing plays into Gandy's concern that a machine specification may not explicitly "reproduce all the sorts of operations which a human computer could perform" -- i.e. his two examples are (i) massively symbol-parallel computation and two-dimensional computation e.g. Conway's "game of life". [cf. Gandy 1978 in (Barwise et al 1980:125)] Therefore there may be processes that can "compute more" than a Turing machine can. See 1980 below.

Kleene defines Turing's Thesis as follows::"§70. Turing's thesis. Turing's thesis that every function which would naturally be regarded as computable under his definition, i.e. by one of his machines, is equivalent to Church's thesis by Theorem XXX."

Indeed immediately before this statement, Kleene states the Theorem XXX:::"Theorem XXX (= Theorems XXVIII + XXIX). The following classes of partial functions are coextensive, i.e. have the same members: (a) the partial recursive functions, (b) the computable functions, (c) the 1/1 computable functions. Similarly with l [lower-case L] completely defined assumed functions Ψ."

Gödel 1963: Only Turing's machines are possible candidates for a use in a definition of "effectively calculable"

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):

:"Note Added 28 August 1963". In consequence of later advances, in particular of the fact that due to A. M. Turing's work⁶⁹ a precise and unquestionably adequate definition of the general notion of formal system⁷⁰ can now be given, a completely general version of Theorems VI and XI is now possible. That is, it can be proved rigorously that in every consistent formal system that contains a certain amount of finitary number theory there exist undecidable arithmetic propositions and that, moreover, the consistency of any such system cannot be proved in the system.

::"⁶⁹ See "Turing 1937", p. 249.

:::"⁷⁰ In my opinion the term "formal system" or "formalism" should never be used for anything but this notion. In a lecture at Princeton (mentioned in "Princeton University 1946", p. 11 [see Davis 1965, pp. 84-88 [i.e. Davis p. 84-88] ] ), I suggested certain transfinite generalizations of formalisms, but these are something radically different from formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle, can be completely replaced by mechanical devices." [Gödel 1963 in (van Heijenoort 1976:616)]

Gödel 1964 -- In Gödel's "Postscriptum" to his lecture's notes of 1934 at the IAS at Princeton [Due to the language difference, Gödel refers to the IAS as "AIS"] , 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:

:"In consequence of later advances, in particular of the fact, that, due to A. M. Turing's work, a precise and unquestionably adequate definition of the general concept of formal system can now be given, the existence of undecidable arithmetical propositions and the non-demonstrability of the consistence of a system in the same system can now be proved rigorously for "every" consistent formal system containing a certain amount of finitary number theory.

:"Turing's work gives an analysis of the concept of "mechanical procedure" (alias "algorithm" or "computation procedure" or "finite combinatorial procedure"). This concept is shown to be equivalent to that of a "Turing machine".* A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas ... the concept of formal system, whose essence it is that reasoning is completely replaced by mechanical operations on formulas. (Note that the question of whether there exist finite "non-mechanical" procedures ... not equivalent with any algorithm, has nothing whatsoever to do with the adequacy of the definition of "formal system" and of "mechanical procedure.

:"... if "finite procedure" is understood to mean "mechanical procedure", the question raised in footnote 3 can be answered affirmatively for recursiveness as defined in §9, which is equivalent to general recursiveness as defined today (see S. C. Kleene (1936) ...)" [Gödel 1934 in (Davis 1967:71-73)]

::" * See A. Turing (1937) ... and the almost simultaneous paper by E. L. Post (1936) ... . As for previous equivalent definitions of computability, which however, are much less suitable for our purpose, see A. Church 1936 ..." [Gödel 1934 in (Davis 1967:72)]

Footnote 3 is in the body of the 1934 lecture notes::"³ The converse seems to be true, if besides recursions according to the scheme (2) recursions of other forms 9e.g., with respect to two variables simultaneously) are admitted. This cannot be proved, since the notion of finite computation is not defined, but it serves as a heuristic principle." [Gödel 1934 in (Davis 1967:44)]

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." [Gödel 1934 in (Davis 1967:40)]

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

Gandy's influential paper titled "Church's Thesis and Principles for Mechanisms" appears in Barwise et al. Given Church's paper (1936) published prior to Turing's "Appendix proof" (1937), then how Gandy arrives at the following expression of Church's Thesis is left to the reader to ponder (see Soare's take on this at 1995). He frames "Church's Thesis" as follows:

"1. Introduction:"Throughout this paper we shall use "calculable" to refer to some intuitively given notion and "computable" to mean "computable by a Turing machine"; of course many equivalent definitions of "computable" are now available.:"Church's Thesis. What is effectively calculable is computable.":" ... Both Church and Turing had in mind calculation by an abstract human being using some mechanical aids (such as paper and pencil" [Gandy in (Barwise 1980:123)]

Gandy attempts to "analyze mechanical processes and so to provide arguments for the following::"Thesis M. What can be calculated by a machine is computable." [Gandy in (Barwise 1980:124]

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".Gandy in (Barwise 1980:126)] But then he restricts his machines even more::"(2) Secondly we suppose that the progress of calculation by a mechanical device may be described in discrete terms, so that the devices considered are, in a loose sense, digital computers.:"(3) Lasty we suppose that the device is deterministic: that is, the subsequent behavior of the device is uniquely determined once a complete description of its initial state is given."Gandy in (Barwise 1980:126)]

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"::"Now we come to the most important of our principles. In Turing's analysis the requirement that the action depended only on a bounded portion of the record was based on a human limitation. We replace this by a physical limitation which we call the "principle of local causation." Its justification lies in the finite velocity of propagation of effects and signals: contemporary physics rejects the possibility of instantaneous action at a distance." [Gandy in (Barwise 1980:135)]

oare 1995

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::"Kleene wrote [1981b, p. 49] , "Turing's computability is intrinsically persuasive" but "λ-definability is not intrinsically persuasive" and "general recursiveness scarcely so (its author Gödel being at the time not at all persuaded) ... . Most people today accept Turing's Thesis" [Soare 1996:13]

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::"⁷Gandy actually wrote "Church's thesis" not "Turing's thesis" as written here, but surely Gandy meant the latter, at least intensionally, because Turing did not prove anything in 1936 or anywhere else about general recursive functions." [Soare 1996:11]

Breger 2000 and the problem of tacit axioms in an "axiomatic system"

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 ..." [Breger in (Groshoz and Breger 2002:221)]

He quotes Hilbert:: "In a university lecture given in 1905, Hilbert considered it "absolutely necessary" to have an "axiom of thought" or "an axiom of the existence of an intelligence" before stating the axioms in logic. In the margin of the script, Hilbert added later: "the a priori of the philosophers." He formulated this axiom as follows: "I have the capacity to think of objects, and to denote them by means of simple symbols like "a, b,..., x, y,...," so that they can be recognized unambiguously. My thought operates with these objects in a certain way according to certain rules, and my thinking is able to detect these rules by observation of myself, and completely to describe these rules" [(Hilbert 1905,219); see also (Peckhaus 1990, 62f and 227)] ." [brackets and references in original, Breger in (Groshoz and Breger 2002:227)]

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. [Breger in (Groshoz and Breger 2002:228)] [Indeed, Breger gives a potent example of this in his paper (Breger in (Groshoz and Breger 2002:228-118))]

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.

ieg 2000 discusses "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 Dedekind and ending in the 1950's with the later papers of Turing and Kleene. The Feferfest paper distills the prior paper to its major points and dwells primarily on Gandy's paper of 1980. Sieg extends Turing's "computability by string machine" (human "computor") as reduced to mechanism "computability by letter machine" [Turing's thesis -- cf drawing p. 398] to the "parallel" machines of Gandy.

Sieg cites more recent work including "Komogorov and Uspensky's work on algorithms" and (De Pisapia 2000), in particular, the KU-pointer machine-model), and artificial neural networksSieig 2002:399] and asserts::"The separation of informal conceptual analysis and mathematical equivalence proof is essential for recognizing that the correctness of "Turing's Thesis" (taken generically) rests on two pillars; namely on the correctness of boundedness and locality conditions for computors, and on the correctness of the pertinent central thesis. The latter asserts explicitly that computations of a computor can be mimicked directly by a particular kind of machine. However satisfactory one may find this line of analytic argument, there are two weak spots: the looseness of the restrictive conditions (What are symbolic configurations? What changes can mechanical operations effect?) and the corresponding vagueness of the central thesis. We are, no matter how we turn ourselves, in a position that is methodologically still unsatisfactory ... ."Sieg 2002:399]

He claims to "step toward a more satisfactory stance ... [by] abstracting further away from particular types of configurations and operations ..."Sieg 2002:399] :"It has been claimed frequently that Turing analyzed computations of machines. That is historically and systematically inaccurate, as my exposition should have made quite clear. Only in 1980 did Turing's student, Robin Gandy, characterize machine computations."Sieg 2002:399]

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::" ... the definition of a Gandy machine is an "abstract" ... definition that embodies ... properties of parallel computations ... Second, Gandy machines share with groups and topological spaces the general feature of abstract axiomatic definitions, namely, that they admit a wide variety of different interpretations. Third, ... the computations of any Gandy machine can be simulated by a letter machine, [and] is best understood as a representation theorem for the axiomatic notion. [boldface added]

:"The axiomatic approach captures the essential nature of computation processes in an abstract way. The difference between the two types of calculators I have been describing is reduced to the fact that Turing computors modify one bounded part of a state, whereas Gandy machines operate in parallel on arbitrarily many bounded parts. The representation theorems guarantee that models of the axioms are computationally equivalent to Turing machines in their letter variety." [Sieg 2002:404]

Notes

References

* Barwise, Jon, H. J. Keisler, and K. Kunen, Editors, 1980, "The Kleene Symposium", 426 pages, North-Holland Publishing Company, Amsterdam, ISBN 0444853456
* Church, A., 1936a, in (Davis 1965:88ff), "An Unsolvable Problem of Elementary Number Theory"
* Church, A., 1936b, in (Davis 1965:108ff), "A Note on the Entscheidungsproblem"
* Church, A., 1938, "The constructive second number class", Bull. Amer. Math. Soc. vol. 44, Number 4, 1938, pp. 224-232]
* Davis, Martin editor, 1965, "The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions", Raven Press, New York, ISBN 0911216014. All the original papers are here including those by Gödel, Church, Turing, Rosser, Kleene, and Post mentioned in this article. Valuable commentary by Davis prefaces most papers.
* Davis, Martin, 2001, "Engines of Logic: Mathematicians and the Origin of the Computer", W. W. Norton & Company, New York, ISBN 0393047857 pbk.
* Dawson, John William, Jr., 1997, "Logical Dilemmas: The Life and Work of Kurt Gödel", 361 pages, A. K. Peters, Wellesley, MA, ISBN 1568810253, QA29.058D39.
* Dawson, John William and John William Dawson, Jr., 2005, "Logical Dilemmas: The Life and Work of Kurt Gödel", 362 pages, A. K. Peters, Wellesley, MA, ISBN 9781568810256
* De Pisapia, N., 2000, "Gandy Machines: an abstract model of parallel computation for Turing Machines, the Game of Life, and Artificial Neural Networks", M.S. Thesis, Carnegie Mellon University, Pittsburgh.
* Dershowitz, Nachum and Gurevich, Yuri, 2007, "A Natural Axiomatization of Church's Thesis", http://research.microsoft.com/~gurevich/Opera/188.pdf
* Gandy, Robin, 1978, "Church's Thesis and the Principles for Mechanisms", in (Barwise et al 1980:123-148)
* George, Alexander (+ed.), 1994, "Mathematics and Mind", 216 pages, New York, Oxford University Press, ISBN 0195079299
* Gödel, K., 1930, in (van Heijenoort 1967:592ff), "Some metamathematical results on completeness and consistency"
* Gödel, K., 1931a, in (Davis 1965:4-38), "On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I."
* Gödel, K., 1931b, in (van Heijenoort 1976:616ff) "On completeness and consistency"
* Gödel, K., 1934, in (Davis 1965:39-74), "On Undecidable Propositions of Formal Mathematical Systems"
* Gödel, K., 1936, in (Davis 1965:82ff), "On The Length of Proofs", "Translated by the editor from the original article in "Ergenbnisse eines mathematishen Kolloquiums", Heft 7 (1936) pp. 23-24." Cited by Kleene (1952) as "Über die Lāange von Beweisen", in "Ergebnisse eines math. Koll", etc.
* Gödel, K., 1964, in (Davis 1965:71ff), "Postscriptum"
* Groshoz, Emily and Breger, Herbert, 2000, "The Growth of Mathematical Knowledge", 416 pages, Kluwer Academic Publishers, Dordrect, The Netherlands, ISBN 0792361512.
* Hawking, Stephen, 2005, "God Created the Integers: The Mathematical Breakthroughs that Changed History, Edited, with Commentary by Stephen Hawking", Running Press, Philadelphia, ISBN 0762419229
* Hodges, Andrew, 1983 , "Alan Turing:The Engima", 1st edition, Simon and Schuster, New York, ISBN 0671528092
* Kleene, S. C., 1935, in (Davis 1965:236ff) "General Recursive Functions of Natural Numbers"
* Kleene, S. C., 1971, 1952 (10th impression 1991) "Introduction to Metamathematics", 550 pages, North-Holland Publishing Company (Wolters-Noordhoff Publishing) ISBN 0720421039
* Merriam-Webster Inc., 1983, "Webster's Ninth New Collegiate Dictionary", 1563 pages, Merriam-Webster Inc., Springfield, MA, ISBN 0-87779-509-6
* Post, E. L., 1936, in (Davis 1965:288ff), "Finite Combinatory Processes - Formulation 1" or The Journal of Symbolic Logic, Vol. 1, No. 3 (Sep., 1936), pp. 103-105.
* Rosser. J. B., 1939, "An informal exposition of proofs of Gödel's Theorem and Church's Theorem", The Journal of Symbolic Logic. Vol. 4. (1939), pp.53-60 and reprinted in (Davis 1967:223-230).
* Sieg, Wilfried, Richard Sommer, and Carolyn Talcott (eds.), 2002, "Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15", 444 pages, A K Peters, Ltd., ISBN 1568811691
* Soare, Robert, 1996, "Computability and Recursion", "Bulletin of Symbolic Logic 2", Volume 2, Number 3, September 1996, pp. 284-321.
* Turing, A., 1937, in (Davis 1965:115ff), "On Computable Numbers, with an application to the Entscheidungsproblem"
* Turing, A., 1939, in (Davis 1965:154ff), "Systems of Logic Based on Ordinals"
* van Heijenoort, Jean, 1976, "From Frege To Gödel: A Source Book in Mathematical Logic", 116 pages, 1879-1931, 3rd Printing, original printing 1967, Harvard University Press, Cambridge Massachusetts, ISBN 0674318447 (pbk.).

External links

[http://www.informatik.uni-trier.de/~ley/db/journals/bsl/index.html The Bulletin of Symbolic Logic] has links to all volumes with papers on line.

[http://www.ams.org/bull/1938-44-04/S0002-9904-1938-06719-5/S0002-9904-1938-06719-5.pdf Alonzo Church, 1938, "The Constructive Second Number Class"] "An address delivered by invitation of the Program Committee at the Indianapolismeeting of the Society, December 29, 1937."

[http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf Kurt Gödel, 1931, "On formally undecidable propositions of Principia Mathematica and related systems I."] Translated by Martin Hirzel, November 27, 2000.

[http://www.ams.org/bull/1946-52-04/S0002-9904-1946-08555-9/S0002-9904-1946-08555-9.pdf Emil L. Post, 1946, "A Variant of a Recursively Unsolvable Problem"]

[http://www.hss.cmu.edu/philosophy/sieg/Church%20without%20dogma.pdf Wilfried Sieg, 2005, "CHURCH WITHOUT DOGMA: Axioms for computability," Carnegie Mellon University]

[http://www.hss.cmu.edu/philosophy/techreports/104_Sieg.pdf Wilfried Sieg, 2000, "Calculations By Man and Machine: conceptual analysis", Carnegie Mellon University]

[http://www.people.cs.uchicago.edu/~soare/References/compute.pdf Robert I. Soare, 1995, "Computability and Recursion"]

[http://www.math.ucla.edu/~asl/bsl/0203/0203-002.ps Robert I. Soare, 1996, "Computability and Recursion"] as it appeared in The Bulletin of Symbolic Logic, Volume 2, Volume 2, Number 3, September 1996.

[http://www.seto.nanzan-u.ac.jp/~sasaki/2004mlg/14-16.pdf Masako Takahashi, 2004, "On general recursive functions", International Christian University] Particularly, see references.

[http://www.thocp.net/biographies/papers/turing_oncomputablenumbers_1936.pdf A. M. Turing, 1936, "On Computable Numbers, with an Application to the Entscheidungsproblem"]