History of the Church–Turing thesis

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 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) ... ."[1]

Observe that in fact Peano's axioms are 9 in number and axiom 9 is the recursion/induction axiom.[2]

"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 ... ."[3]

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 "Entscheidungsproblem" (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]".[4] Because of this, "the consistency of P is unprovable in P, provided P is consistent".[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.

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.[6]"

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[7] proved that Frege's rules were complete "... in the sense that every valid formula is provable".[8] 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".[9]

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".[10]

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

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."[11]

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."[12]

In subsequent years Kleene[13] 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."[14]

Kleene concludes[15] 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.

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."[16]

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:

"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[17])."[18]

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[19] 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 ..."[20]

Dawson states that these lectures were meant to clarify concerns that the "incompleteness theorems were somehow dependent on the particularities of formalization":[21]

"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 ...[22] 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,[23] 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 (Turing 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]."[24]

Kleene and Rosser transcribed Gödel's 1934 lectures in Princeton. In his paper General Recursive Functions of Natural Numbers[25] 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 ...[26]

"A recursive function (relation) in the sense of Gödel ... will now be called a primitive recursive function (relation).[27]

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":[28]

"³ 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."[29]

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."[30]

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."[31]

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".[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. The worker is equipped with "a fixed unalterable set of directions".[33] 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"[33] 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 recursiveness.⁸" (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."[34]

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."[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. 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"[36] 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."[37]

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",[38] 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."[36]

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 squares 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."[39]

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

"A number is computable if it differs by an integer from the number computed by a circle-free machine."[40]

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."[38]

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."[41]

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.

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 mechanical 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.[42]

"† 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."[43]

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

J. B. Rosser's paper An Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem[44] 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]."[45]

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][46]

²³ Turing [1] [On Computable numbers, with an application to the Entscheidungsproblem(1936)][47]

²⁴ Post [1, p. 105],[48] and Church [2] [49]

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."[50]

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)."[51]

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."[52]

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."[53]

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

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."[54]

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). 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) ...)" [56]

" * See 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 ..."[57]

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 (e.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."[58]

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."[59]

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:

"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)"[60]

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:

"Thesis M. What can be calculated by a machine is computable."[61]

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".[62] 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."[62]

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."[63]

In 1985 the "Thesis M" was adapted for Quantum Turing machine, resulting in a Church–Turing–Deutsch principle.

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"[64]

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."[65]

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 ..."[66]

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)]."[67]

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.[68][69]

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.

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"[70] 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[71] 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 ... ."[71]

He claims to "step toward a more satisfactory stance ... [by] abstracting further away from particular types of configurations and operations ..."[71]

"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."[71]

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" mathematical 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."[72]

• Barwise, Jon, H. J. Keisler, and K. Kunen, Editors, 1980, The Kleene Symposium, 426 pages, North-Holland Publishing Company, Amsterdam, ISBN 0-444-85345-6
• 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 0-911216-01-4. 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 0-393-04785-7 pbk.
• Dawson, John William, Jr., 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, 361 pages, A. K. Peters, Wellesley, MA, ISBN 1-56881-025-3, 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 978-1-56881-025-6
• 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 0-19-507929-9
• 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 0-7923-6151-2.
• Hawking, Stephen, 2005, God Created the Integers: The Mathematical Breakthroughs that Changed History, Edited, with Commentary by Stephen Hawking, Running Press, Philadelphia, ISBN 0-7624-1922-9
• Hodges, Andrew, 1983 , Alan Turing:The Enigma, 1st edition, Simon and Schuster, New York, ISBN 0-671-52809-2
• 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 0-7204-2103-9
• 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 1-56881-169-1
• Soare, Robert, 1996, Computability and Recursion, "Bulletin of Symbolic Logic 2", Volume 2, Number 3, September 1996, pp. 284–321.
• Turing, A. M. (1937) [Delivered to the Society 1936], "On Computable Numbers, with an Application to the Entscheidungsproblem" (PDF), Proceedings of the London Mathematical Society, 2, vol. 42, pp. 230–65, doi:10.1112/plms/s2-42.1.230, S2CID 73712 and Turing, A.M. (1938). "On Computable Numbers, with an Application to the Entscheidungsproblem: A correction". Proceedings of the London Mathematical Society. 2. Vol. 43 (published 1937). pp. 544–6. doi:10.1112/plms/s2-43.6.544. (See also: Davis 1965:115ff)
• 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 0-674-31844-7 (pbk.).

• The Bulletin of Symbolic Logic has links to all volumes with papers on line.
• Alonzo Church, 1938, The Constructive Second Number Class "An address delivered by invitation of the Program Committee at the Indianapolis meeting of the Society, December 29, 1937."
• Kurt Gödel, 1931, On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Martin Hirzel, 27 November 2000.
• Emil L. Post, 1946, A Variant of a Recursively Unsolvable Problem
• Wilfried Sieg, 2005, CHURCH WITHOUT DOGMA: Axioms for computability, Carnegie Mellon University
• Wilfried Sieg, 2000, Calculations By Man and Machine: conceptual analysis, Carnegie Mellon University
• Robert I. Soare, 1995, Computability and Recursion
• Robert I. Soare, 1996, Computability and Recursion as it appeared in The Bulletin of Symbolic Logic, Volume 2, Volume 2, Number 3, September 1996.
• Masako Takahashi, 2004, On general recursive functions, International Christian University Particularly, see references.
• A. M. Turing, 1936, On Computable Numbers, with an Application to the Entscheidungsproblem