History of the Church–Turing thesis


The history of the Church–Turing thesis involves the history of the development of the study of the nature of functions whose values are effectively calculable; or, in more modern terms, functions whose values are algorithmically computable. It is an important topic in modern mathematical theory and computer science, particularly associated with the work of Alonzo Church and Alan Turing.
The debate and discovery of the meaning of "computation" and "recursion" has been long and contentious. This article provides detail of that debate and discovery from Peano's axioms in 1889 through recent discussion of the meaning of "axiom".

Peano's nine axioms of arithmetic

In 1889, Giuseppe Peano presented his The principles of arithmetic, presented by a new method, based on the work of Dedekind. Soare proposes that the origination of "primitive recursion" began formally with the axioms of Peano, although
Observe that in fact Peano's axioms are 9 in number and axiom 9 is the recursion/induction axiom.

Hilbert and the [Entscheidungsproblem]

At the International Congress of Mathematicians 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. 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", "there exist undecidable sentences ". Because of this, "the consistency of P is unprovable in P, provided P is consistent". While Gödel’s proof would display the tools necessary for Alonzo Church and Alan Turing to resolve the 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." Although stated easily nowadays, the question would float about for almost 30 years before it was framed precisely.
Hilbert's original description of problem 10 begins as follows:
By 1922, the specific question of an "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 a set of axioms and a logical conclusion written in first-order logic, that is—written in what Davis calls "Frege's rules of deduction". Gödel’s doctoral dissertation proved that Frege's rules were complete "... in the sense that every valid formula is provable". Given that encouraging fact, could there be a generalized "calculational procedure" that would tell us whether a conclusion can be derived from its premises? Davis calls such calculational procedures "algorithms". The Entscheidungsproblem would be an algorithm as well. "In principle, an algorithm for Entscheidungsproblem would have reduced all human deductive reasoning to brute calculation".
In other words: Is there an "algorithm" that can tell us if any formula is "true"
Indeed: What about our Entscheidungsproblem algorithm itself? Can it determine, in a finite number of steps, whether it, itself, is “successful” and "truthful" ?

Three problems from Hilbert's 2nd and 10th problems

At the 1928 Congress Hilbert refines the question very carefully into three parts. The following is Stephen Hawking's summary:
and Wilhelm Ackermann display recursive functions that are not primitive recursive:
In subsequent years Kleene observes that Rózsa Péter simplified Ackermann's example and Raphael Robinson. Péter exhibited another example that employed Cantor's diagonal argument. Péter and Ackermann also displayed "transfinite recursions", and this led Kleene to wonder:
Kleene concludes that all "recursions" involve the formal analysis he presents in his §54 Formal calculations of primitive recursive functions and, the use of mathematical induction. He immediately goes on to state that indeed the Gödel-Herbrand definition does indeed "characterize all recursive functions" – see the quote in [|1934, below].

Gödel's proof

In 1930, mathematicians gathered for a mathematics meeting and retirement event for Hilbert. As luck would have it,
He announced that the answer to the first two of Hilbert's three questions of 1928 was NO.
Subsequently in 1931 Gödel published his famous paper In his preface to this paper Martin Davis delivers a caution:

Gödel expansion of "effective calculation"

To quote Kleene, "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". Gödel delivered a series of lectures at the Institute for Advanced Study, Princeton NJ. In a preface written by Martin Davis Davis observes that
Dawson states that these lectures were meant to clarify concerns that the "incompleteness theorems were somehow dependent on the particularities of formalization":

Kleene

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

Church definition of "effectively calculable"

paper An Unsolvable Problem of Elementary Number Theory proved that the Entscheidungsproblem was undecidable within the λ-calculus and Gödel-Herbrand's general recursion; moreover Church cites two theorems of Kleene's that proved that the functions defined in the λ-calculus are identical to the functions defined by general recursion:
The paper opens with a very long footnote, 3. Another footnote, 9, is also of interest. Martin Davis states that "This paper is principally important for its explicit statement that the functions which can be computed by a finite algorithm are precisely the recursive functions, and for the consequence that an explicit unsolvable problem can be given":
Footnote 9 is in section §4 Recursive functions:
Some time prior to Church's paper An Unsolvable Problem of Elementary Number Theory 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 we see, under the chapter §7 The notion of effective calculability, a footnote 18 which states the following:
By "identifying" Church means – not "establishing the identity of" – but rather "to cause to be or become identical", "to conceive as united" , and as "to be or become the same".

Post and "effective calculability" as "natural law"

doubts as to whether or not recursion was an adequate definition of "effective calculability", plus the publishing of Church's paper, encouraged him in the fall of 1936 to propose a "formulation" with "psychological fidelity": A worker moves through "a sequence of spaces or boxes" performing machine-like "primitive acts" on a sheet of paper in each box. The worker is equipped with "a fixed ualterable set of directions". Each instruction consists of three or four symbols: an identifying label/number, an operation, next instruction ji; however, if the instruction is of type and the determination is "yes" THEN instruction ji' ELSE if it is "no" instruction ji. The "primitive acts" are of only 1 of 5 types: mark the paper in the box he's in, erase the mark, move one room to the right, move one room to the left, 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.
This matter, mentioned in the introduction about "intuitive theories" caused Post to take a potent poke at Church:
In other words Post is saying "Just because you defined it so doesn't make it truly so; your definition is based on no more than an intuition." Post was searching for more than a definition: "The success of the above program would, for us, change this hypothesis not so much to a definition or to an axiom but to a natural law. Only so, it seems to the writer, can Gödel's theorem... and Church's results... be transformed into conclusions concerning all symbolic logics and all methods of solvability."
This contentious stance finds grumpy expression in Alan Turing 1939, and it will reappear with Gödel, Gandy, and Sieg.

Turing and computability

paper 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". But he uses the word "computation" in the context of his machine-definition, and his definition of "computable" numbers is as follows:
What is Turing's definition of his "machine?" Turing gives two definitions, the first a summary in §1 Computing machines and another very similar in §9.I derived from his more detailed analysis of the actions a human "computer". With regards to his definition §1 he says that "justification lies in the fact that the human memory is necessarily limited", and he concludes §1 with the bald assertion of his proposed machine with his use of the word "all"
The emphasis of the word one in the above brackets is intentional. With regards to §9.I he allows the machine to examine more squares; it is this more-square sort of behavior that he claims typifies the actions of a computer :
Turing goes on to define a "computing machine" in §2 is "a-machine" as defined in §1 with the added restriction : It prints two kinds of symbols – figures 0 and 1 – and other symbols. The figures 0 and 1 will represent "the sequence computed by the machine".
Furthermore, to define the if the number is to be considered "computable", the machine must print an infinite number of 0's and 1's; if not it is considered to be "circular"; otherwise it is considered to be "circle-free":
Although he doesn't call it his "thesis", Turing proposes a proof that his "computability" is equivalent to Church's "effective calculability":
The Appendix: Computability and effective calculability begins in the following manner; observe that he does not mention recursion here, and in fact his proof-sketch has his machine munch strings of symbols in the λ-calculus and the calculus munch "complete configurations" of his machine, and nowhere is recursion mentioned. The proof of the equivalence of machine-computability and recursion must wait for Kleene 1943 and 1952:
Gandy seems to confuse this bold proof-sketch with Church's Thesis; see 1960 and 1995 below. Moreover a careful reading of Turing's definitions leads the reader to observe that Turing was asserting that the "operations" of his proposed machine in §1 are sufficient to compute any computable number, and the machine that imitates the action of a human "computer" as presented in §9.I is a variety of this proposed machine. This point will be reiterated by Turing in 1939.

Turing identifies effective calculability with machine computation

massive Princeton PhD thesis 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 the notions of "machine computation" and "effectively calculable".
This is a powerful expression. because "identicality" is actually an unequivocal statement of necessary and sufficient conditions, in other words there are no other contingencies to the identification" except what interpretation is given to the words "function", "machine", "computable", and "effectively calculable":

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

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

Kleene and ''Thesis I''

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

Kleene and Church and Turing theses

In his chapter §60, Kleene defines the "Church's thesis" as follows:
On page 317 he explicitly calls the above thesis "Church's thesis":
About Turing's "formulation", Kleene says:
Kleene proposes that what Turing showed: "Turing's computable functions 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."
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 massively symbol-parallel computation and two-dimensional computation e.g. Conway's "game of life". Therefore there may be processes that can "compute more" than a Turing machine can. See 1980 below.
Kleene defines Turing's Thesis as follows:
Indeed immediately before this statement, Kleene states the Theorem XXX:

Gödel, Turing machines, and effectively calculability

To his 1931 paper On Formally Undecidable Propositions, Gödel added a Note added 28 August 1963 which clarifies his opinion of the alternative forms/expression of "a formal system". He reiterates his opinions even more clearly in 1964 :
Gödel 1964 – In Gödel's Postscriptum to his lecture's notes of 1934 at the IAS at Princeton, he repeats, but reiterates in even more bold terms, his less-than-glowing opinion about the efficacy of computability as defined by Church's λ-definability and recursion. This was in a letter to Martin Davis. The repeat of some of the phrasing is striking:
Footnote 3 is in the body of the 1934 lecture notes:
Davis does observe that "in fact the equivalence between his definition and Kleene's is not quite trivial. So, despite appearances to the contrary, footnote 3 of these lectures is not a statement of Church's thesis."

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

's influential paper titled Church's Thesis and Principles for Mechanisms appears in Barwise et al. Gandy starts off with an unlikely expression of Church's Thesis, framed as follows:
Robert Soare had issues with this framing, considering Church's paper published prior to Turing's "Appendix proof".
Gandy attempts to "analyze mechanical processes and so to provide arguments for the following:
Gandy "exclude from consideration devices which are essentially analogue machines....The only physical presuppositions made about mechanical devices 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 on the speed of propagation of change". But then he restricts his machines even more:
He in fact makes an argument for this "Thesis M" that he calls his "Theorem", the most important "Principle" of which is "Principle IV: Principle of local causation":
In 1985 the "Thesis M" was adapted for Quantum Turing machine, resulting in a Church–Turing–Deutsch principle.

Soare

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

Breger and problem of tacit axioms

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

Sieg and axiomatic definitions

At the "Feferfest" – Solomon Feferman's 70th birthday – Wilfried Sieg first presents a paper written two years earlier titled "Calculations By Man and Machine: Conceptual Analysis", reprinted in. Earlier Sieg published "Mechanical Procedures and Mathematical Experience" 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" as reduced to mechanism "computability by letter machine" to the parallel machines of Gandy.
Sieg cites more recent work including "Kolmogorov and Uspensky's work on algorithms" and, and artificial neural networks and asserts:
He claims to "step toward a more satisfactory stance... abstracting further away from particular types of configurations and operations..."
Whether the above statement is true or not is left to the reader to ponder. Sieg goes on to describe Gandy's analysis. In doing so he attempts to formalize what he calls "Gandy machines". About the Gandy machines: