Typed letter signed ‘Kurt Gödel’ to Martin Davis, with manuscript annotations by both Gödel and Davis, on Gödel’s contributions to Davis’ book The Undecidable, and in particular Gödel’s opinions on the ‘Church-Turing thesis’.

Princeton, New Jersey: The Institute for Advanced Study, February 15, 1965.

A highly important letter from Gödel to the logician Martin Davis in which Gödel clarifies his position on ‘Church’s thesis’ (later called the Church-Turing thesis), which proposed an answer to the question of what constitutes ‘effective calculability’. From February to May 1934, Gödel lectured at the Institute for Advanced Study on his epoch-making undecidability results of three years earlier. Mimeographed lecture notes were circulated at the time, but the lectures were not formally published until 1965, in the book The Undecidable, edited by Davis. As Gödel later wrote, “A number of misprints and oversights in the original mimeographed lecture notes were corrected when they were reprinted in [The Undecidable]. I am indebted to Professor Martin Davis for calling my attention to some of them” (Kurt Gödel CollectedWorks I, p. 371). The present letter sets out Gödel’s corrections and emendations to the original lectures, for Davis to incorporate in the published version. In the lectures, Gödel noted that primitive recursive functions “have the important property that, for each given set of values of the arguments, the value of the function can be computed by a finite procedure.” To this remark Gödel added a footnote that suggested that a converse of this statement could serve as a “heuristic principle”. When Davis submitted to Gödel a preliminary version of his introduction to Gödel’s lectures, he suggested that this footnote, together with his proposed definition of general recursive function in the same lectures, amounted to a precise characterization of the mechanically calculable functions and hence to a statement of Church’s thesis. However, “Gödel in 1934 did not subscribe to Church’s thesis, which as formulated in terms of lambda-definability Church had proposed to him in a personal communication around February or March 1934. Thus, Gödel wrote on 15 February 1965 to Davis [in the offered letter], ‘it is not true that footnote 3 is a statement of Church’s Thesis. The conjecture stated there only refers to the equivalence of ‘finite (computation) procedure’ and ‘recursive procedure’. However, I was, at the time of these lectures, not at all convinced that my concept of recursion comprises all possible recursions; and in fact the equivalence between my definition and Kleene’s in Math. Ann. 112 (1936) is not quite trivial’” (quoted by Kleene, in ibid., p. 341). “Gödel was unconvinced by Church’s thesis, since it did not rest on a direct conceptual analysis of the notion of finite algorithmic procedure … Indeed, in his Princeton lectures Gödel said that the notion of effectively computable function could serve just as a heuristic guide. It was only when Turing, in 1937, offered the definition in terms of his ‘machines’ that Gödel was ready to accept such an identification, and thereafter he referred to Turing’s work as having provided the ‘precise and unquestionably adequate definition of formal system’ by his ‘analysis of the concept of 'mechanical procedure’ needed to give a general formulation of the incompleteness results’” (Fefermann in ibid., p. 33). As Gödel himself later wrote in a Postscriptum to the 1934 lectures, “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 with general recursiveness as defined today” (ibid., p. 370). 

In 1923-33, Alonzo Church presented a new system of logic. “At the time Church thought that his system – which he regarded as a ‘radically different formulation of logic’– might escape the strictures of Gödel’s incompleteness results, for he ‘thought that Gödel[’s] ... theorem[s] might be found to depend on peculiarities of type theory,’ a theory whose ‘unfortunate restrictiveness’ he sought to overcome.

“By the fall of 1933 the consistency of Church’s full formal system had begun to be suspect, and in the spring of 1934 Kleene and J. B. Rosser, another of Church’s graduate students, showed that it was, in fact, inconsistent – a discovery that forced Kleene to have to rewrite his dissertation. Nevertheless, the subsystem known as the λ-calculus came through unscathed, and with it all the results that Kleene had obtained on the λ-definability of a great variety of effectively calculable functions.

“Reportedly, those results were ‘circulating among the logicians at Princeton’ when Gödel arrived there, and it was on the basis of them that Church was emboldened to propose his ‘Thesis’ that all effectively calculable functions are λ-definable (and hence that the informal notion of effective calculability is equivalent to the formal one of λ-definability). Gödel, however, was skeptical, as Church himself noted in a contemporary account of the evolution of the theory of λ-definability: ‘My proposal . . . he regarded as thoroughly unsatisfactory. I replied that if he would propose any definition of effective calculability which seemed even partially satisfactory I would undertake to prove that it was included in lambda-definability.’

“In fact, that was just what happened. For though Gödel’s ‘only idea at the time was that it might be possible ... to state a set of axioms which would embody the generally accepted properties’ of effective calculability, ‘it occurred to him later that Herbrand’s definition of recursiveness . . . could be modified in the direction of effective calculability’. He presented the idea at the end of the course of lectures he gave at the IAS the following spring.

“When Gödel’s course of lectures began Kleene had just returned to Princeton after a seven-month absence, and he and Rosser were recruited by [Oswald] Veblen to serve as note-takers for the course. The notes themselves were distributed in mimeographed installments to those who subscribed for them, as well as to a few libraries. Subsequently they circulated widely, but they were not published until 1965, in Martin Davis’s anthology The Undecidable.

“Although the subject matter of the 1934 lectures was essentially that of Gödel’s paper [of 1931], a comparison of the titles of the two works suggests the broader scope of the later treatment: ‘On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I’ (1931) versus ‘On Undecidable Propositions of Formal Mathematical Systems’ (1934). Since even so distinguished a logician as Church was among those who thought that the incompleteness theorems were somehow dependent on the particularities of formalization, it was surely one of Gödel’s principal aims in the 1934 lectures to dispel doubts about the generality of the incompleteness phenomena. Accordingly, although he did discuss one particular formal system as an example of those to which his considerations would apply, in the very first paragraph of the 1934 paper he defined a formal mathematical system quite generally, as ‘a system of symbols together with rules for employing them,’ where the rules of deduction and the definitions of what were to constitute meaningful formulas and axioms were to be specified constructively (that is, in terms of finitary decision procedures).

“As he had in the earlier paper, Gödel proceeded to define the class of functions now called primitive recursive but that he simply called recursive – functions that, he stressed, ‘have the important property that, for each given set of values of the arguments, the value of the function can be computed by a finite procedure.’ He was aware, however, that not all functions with that property were primitive recursive, since during the period 1927–28 Wilhelm Ackermann (and, independently and almost simultaneously, Gabriel Sudan) had given examples of effectively computable functions, defined by means of multiple or nested recursions, that grew too fast to be primitive recursive. 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 converse seems to be true, if besides [primitive] recursions … 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.’

“The conjecture has since elicited much comment. In particular, when Martin Davis undertook to publish Gödel’s 1934 lectures he took it to be a variant of Church’s Thesis; but in a letter to Davis [the offered letter] 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, 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 (On computable numbers, 1937).

“Gödel’s reluctance to regard either general recursiveness or λ-definability as adequate characterizations of the informal notion of effective computability has been examined in detail by several authors. There is a consensus that, in fact, neither Gödel’s nor Church’s formalisms were so perspicuous or intrinsically persuasive as 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 Turing all turned out to have the same extension) is less compelling than has generally been supposed. Hence, quite apart from Gödel’s innate caution, there were good reasons for his skepticism …

[Gödel’s] hindsightful remarks at the Princeton Bicentennial Conference [‘Remarks Before the Princeton Bicentennial Conference on Problems of Mathematics,’ pp. 84-88 in The Undecidable] suggest that he simply did not expect it to be possible to give ‘an absolute definition of an interesting epistemological notion.’ That general recursiveness turned out to do just that – in particular, that ‘the diagonal procedure [did] not lead outside’ the class of (partial) recursive functions – seemed to him ‘a kind of miracle.’ Thus, in defining the class of general recursive functions it was not his aim to capture all possible recursions, for to attempt to do so would, in his view, have been to pursue a phantom” (Dawson, pp. 99-102).

Gödel has added a manuscript note at the end of the present letter referring to his lecture at the Princeton Bicentennial Conference: “The few changes I made in my Bicentennial Lecture are purely stilistic [sic]”.

The letter reads, in full:

Dear Professor Davis,

I am returning herewith the proof sheets of the two Kolloquium Notes and of my Bicentennial Lecture. I made a few alterations in your translation. I think the new wordings correspond more closely with the German original, and also express the meaning more clearly.

I don’t agree at all with section (3) of your introduction. There is not only [in the Princeton lectures] “an effort to obtain undecidability results for formal mathematical systems in general”. Rather there is in section 6 a quite precise result which is so general that it suffices for all applications occurring in practice. Moreover (for languages using variables for integers) the most general result can be obtained very easily from mine simply by leaving out one condition; see the postscript.

As far as the second half of section (3) is concerned, it is not true that footnote 3 is a statement of Church’s Thesis. The conjecture stated there only refers to the equivalence of ‘finite (computation) procedure’ and ‘recursive procedure’. However, I was, at the time of these lectures, not at all convinced that my concept of recursion comprises all possible recursion; and in fact the equivalence between my definition and Kleene’s in Math. Ann. 112 (1936) is not quite trivial.

It seems to me that in the enumeration of the “points of novelty” the transformation of the undecidable proposition into a problem about a Diophantine equation, and perhaps also the avoidance of the italicizing scheme used in my original paper should be mentioned. Moreover some of the new footnotes will probably interest the reader: you mention, however, only “corrections and minor emendations.” Also I think that “much simpler” in section (1) of your introduction is an overstatement [Davis wrote: “the specific formal system chosen as example (although again based on the theory of types) permits variables ranging over numerical-valued functions; this makes it possible to give a much simpler proof than before that recursive (i.e. primitive recursive) functions are representable in the system”].

I hope all changes and additions I made in the proof sheets of my 1934 lecture notes have been incorporated in the final text. I have not yet notified you of a few further corrections and additions I made in the manuscript before sending it to Professor Shepherdson and other publishers.

These are the following:

  1. I added a new footnote. See No. 11 on the sheet of additions enclosed herewith.
  2. I inserted “up to transformations by the arithmetical rules of computation” after “if” in footnote 17 on p. 22 of the original edition.
  3. I inserted “his” before “footnote 5” in the extended footnote on Herbrand’s two definitions (p. 26 of the original edition).
  4. In the postscript I replaced:

a) The first 5 lines of p. 2 as indicated on the sheet enclosed.

b) “quoted” by “cited” in line 6, from below, of p. 2.

c) “mentioned” by “just-mentioned” in the last line of p. 1.

d) Moreover the commas after “algorithm”, “mentioned”, and “moreover” in the fourth line from below of p. 1, and the second line of p. 2 respectively, should be deleted.

I don’t think I shall spend any more time on these lecture notes, so that this may be considered their final form.

As far as the translation of my 1931 paper is concerned, it is not quite so good as I had expected. Some improvements would certainly be desirable, and I have also found an error. It is not my intention to revise a second translation carefully. I am really surprised that I was not consulted at all about this matter, although the publishers engaged a translator expressly for this purpose. Would Professor van Heijenoort or Harvard University Press object to the use of their translation [published in 1967 in From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931]?

Incidentally, it occurred to me that I have never seen a table of contents of the title of the proposed book. Could you supply these to me?

Sincerely yours,

Kurt Gödel.

Kurt Gödel (1906-78) was an Austrian-born mathematician, logician, and philosopher. Gödel left Austria at the outbreak of World War I and, with Einstein’s help, took up a position at the Institute for Advanced Study, where he remained until his retirement in 1976.

Gödel “obtained what may be the most important mathematical result of the 20th century: his famous incompleteness theorem, which states that within any axiomatic mathematical system there are propositions that cannot be proved or disproved on the basis of the axioms within that system; thus, such a system cannot be simultaneously complete and consistent. This proof established Gödel as one of the greatest logicians since Aristotle, and its repercussions continue to be felt and debated today” (Britannica). In his doctoral thesis, ‘Über die Vollständigkeit des Logikkalküls’ (‘On the Completeness of the Calculus of Logic’), published in a slightly shortened form in 1930, Gödel proved one of the most important logical results of the century—indeed, of all time—namely, the completeness theorem, which established that classical first-order logic, or predicate calculus, is complete in the sense that all of the first-order logical truths can be proved in standard first-order proof systems. This, however, was nothing compared with what Gödel published in 1931—namely, the incompleteness theorem: ‘Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I’ (‘On Formally Undecidable Propositions of Principia Mathematica and Related Systems’)” (Britannica).

“The immediate effect of Gödel’s theorem was that the assumptions of Hilbert’s program were challenged. Hilbert assumed quite explicitly that arithmetic was complete in the sense that it would settle all questions that could be formulated in its language—it was an open problem he was confident could be given a positive solution … up to 1930 it was widely assumed that arithmetic, analysis, and indeed set theory could be completely axiomatized, and that once the right axiomatizations were found, every sentence of the theory under consideration could be either proved or disproved in the object-language theory itself. Gödel’s theorem showed that this was not so … Gödel’s results had a profound influence on the further development of the foundations of mathematics” (Zach, pp. 923-4).

“Martin Davis [wa]s one of the world’s outstanding logicians. He was born in 1928 in New York City, where he attended City College and was influenced by Emil L. Post. Early on, Davis came under the spell of Hilbert’s Tenth Problem: Does there exist an algorithm that can, given an arbitrary Diophantine equation, decide whether that equation is solvable? Davis’s Ph.D. dissertation, written at Princeton University under the direction of Alonzo Church, contained a conjecture that, if true, would imply that Hilbert’s Tenth Problem is unsolvable. In rough terms, the conjecture said that any computer can be simulated by a Diophantine equation. The implications of this conjecture struck many as unbelievable, and it was greeted with a good deal of skepticism; for example, the conjecture implies that the primes are the positive part of the range of a Diophantine polynomial. Work during the 1950s and 1960s by Davis, Hilary Putnam, and Julia Robinson made a good deal of headway towards proving the conjecture. The final piece of the puzzle came with work of Yuri Matiyasevich, in 1970” (‘Interview with Martin Davis’, Notices of the American Mathematical Society, Vol. 55, No. 5, May 2008, pp. 560-571).

Davis recounts the context of the present letter: “As a young man committed to making mathematical logic my life's work, Gödel was a towering and inspirational figure. I was also thrilled to be part of the circle at the Institute for Advanced Studies at Princeton, and to see Einstein and Gödel walking together. Many years later, I was editing an anthology of fundamental research papers, The Undecidable (1965), all concerned with the new perspectives that Gödel's revolutionary 1931 paper on formally undecidable propositions had illuminated. Several of the articles included were by Gödel himself. The book was entirely in English although three of Gödel's contributions had been originally published in German, and I translated two of these. I was pleased when during our correspondence he approved my translations. He also wrote me adding a significant amount of new material to another article (one that had originated in a series of lectures given in English at the Institute of Advanced Study in Princeton in 1934), bringing it up to date, emphasizing the importance of Alan Turing's work in extending the incompleteness theorem” (https://www.bonhams.com/auction/26073/lot/98/godel-kurt-1906-1978-archive-of-correspondence-and-notes-sent-to-dr-martin-davis/).

Davis, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, 1965 (this included five pieces by Gödel as well as material by Alan Turing, Alonzo Church, Emil Post, Stephen K. Kleene and J.B. Rosser).Dawson, Logical Dilemmas. The Life and Work of Kurt Gödel, 1997. Fefermann et al. (eds.), Kurt Gödel Collected Works. Volume I. Publications 1929-1936, 1986. Zach, ‘Kurt Gödel, Paper on the Incompleteness Theorems (1931),’ pp. 917-925 in Landmark Writings in Western Mathematics 1640-1940, I. Grattan-Guinness (ed.), 2005.



4to (280 x 218 mm), pp. 2. Stapled (light creasing, staple-related tears in upper left corner).

Item #6293

Price: $25,000.00