Skip to main content
SpringerLink
Log in
SpringerLink
Log in

In the Shadow of Incompleteness: Hilbert and Gentzen

  • Chapter
  • First Online:
Epistemology versus Ontology

Part of the book series: Logic, Epistemology, and the Unity of Science ((LEUS,volume 27))

Abstract

Gödel’s incompleteness theorems had a dramatic impact on Hilbert’s foundational program. That is common lore. For some, e.g. von Neumann and Herbrand, they undermined the finitist consistency program; for others, e.g. Gödel and Bernays, they left room for a fruitful development of proof theory. This paper aims for a nuanced and deepened understanding of how Gödel’s results effected a transformation of proof theory between 1930 and 1934. The starting-point of this transformative period is Gödel’s announcement of a restricted unprovability result in September of 1930; its end-point is the completion of Gentzen’s first consistency proof for elementary number theory in late 1934. Hilbert, surprisingly, is the initial link between starting-point and end-point. He addressed Godelian issues in two strikingly different papers, (1931a) and (1931b), without mentioning Gödel. In (1931a) he takes on the challenge of the restricted unprovability result; in (1931b) he responds to the second incompleteness theorem concerning the unprovability of consistency for a system S in S. He does so by bringing in semantic considerations and by pursuing novel, but also highly problematic directions: he argues for the contentual correctness of a constructive (for him, finitist) theory that includes intuitionist number theory. Gentzen followed the new directions in late 1931, addressed methodological issues and metamathematical problems in ingenious ways, while building on ideas and techniques that had been introduced in proof theory. Most distinctive is Gentzen’s struggle with contentual correctness and its relation to consistency. That is reflected in a sequence of notes Gentzen wrote between late-1931 and late-1934, but it is also central in his classical paper (1936). The immediate lessons seem to be: (i) there is real continuity between Hilbert’s proof theory and Gentzen’s work, and (ii) there is deepened concern for interpreting intuitionist arithmetic (and thus understanding classical arithmetic) from a more strictly constructive perspective. Ironically, the latter concern deeply influenced Gödel’s functional interpretation of intuitionist arithmetic.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In Fall 2009, I wrote an Introduction to late Hilbert papers for (Hilbert 2011) and presented, on 6 November 2009, a version in a talk (with the same title as this essay) to the Workshop on Logical Methods in the Humanities at Stanford University. The present essay expands that paper.

  2. 2.

    However, it could not have been written without Menzler-Trott’s historical work, von Plato’s discovery of Gentzen’s Urdissertation, and Thiel’s efforts to establish a Gentzen Nachlass and to transcribe early manuscripts. I am grateful to all three, but in particular to Thiel for sending me, in the middle of December 2009, the important manuscript INH. Von Plato was deeply involved in its transcription and pointed out to me, why he considers it as very significant. INH and other manuscripts will be made available, I hope very soon, in a full edition of Gentzen’s Nachlass.

  3. 3.

    Many thanks are also due to Sabine Friedrich, Ulrich Majer, Wilfried Nippel, Winfried Schultze, and Marion Sommer for exploring archival questions in Berlin, Göttingen, and Hamburg. For pertinent remarks, suggestions and additional information I thank Wilfried Buchholz, Martin Davis, John Dawson, Heinz-Dieter Ebbinghaus, Eckart Menzler-Trott, Grigori Mints, William Tait, and Christian Thiel.

  4. 4.

    See my paper Hilbert’s proof theory. All the Hilbert lectures I am referring to are contained in (Hilbert 2011).

  5. 5.

    The first step in this and later consistency proofs is the transformation of linear derivations into tree-like structures. That is achieved through the “Auflösung in Beweisfäden”. The structure of the argument is discussed not only in these lecture notes, but also in (Hilbert 1923, p. 1142) and (Ackermann 1924, section II); it is beautifully presented in (Hilbert and Bernays 1934, pp. 221–228).

  6. 6.

    A formula is called numeric if it contains neither bound nor free variables.

  7. 7.

    Ackermann’s paper was submitted for publication on 30 March 1924 and von Neumann’s on 29 July 1925.

  8. 8.

    Hilbert gave lecture courses on Grundlagen der Mathematik in the winter term 1927/1928 and on Mengenlehre in the summer term of 1929. There are no notes for the 1927/1928 lectures, but for the set theory course Menzler-Trott describes in his (2007, Note 8, p. 22) detailed notes that were taken by Lothar Collatz; see (Hilbert* 1929). Apart from their mathematical value, these notes are of special interest in the context of this paper, as Gentzen attended these lectures with his friend Collatz; cf. section 5.

  9. 9.

    (Hilbert 1927, p. 477). Hilbert continues: Diese Ersetzungen werden nach erfolgter Elimination der freien Variablen durch schrittweises Probieren gefunden, und es muß gezeigt werden, daß dieser Prozeß jedenfalls zu einem Abschluß führt. – This is the fact that has to be established by “a purely mathematical finiteness proof”. – A careful discussion is given in (Avigad and Zach 2007), and a beautiful contemporary presentation of the method is found in (Tait 2010).

  10. 10.

    Bernays reemphasizes this point in the later discussion surrounding the second incompleteness theorem, when writing on 20 April 1931 to Gödel: “That proof [of Ackermann] – to which Hilbert referred in his lecture on The Foundations of Mathematics [i.e., in (Hilbert 1927)] with the addendum appended by me – I have repeatedly considered and viewed as correct.” – Ackermann never published his second proof; it was only presented in the second volume of Grundlagen der Mathematik in section 2, see (Hilbert and Bernays 1939, pp. 121–130, and note 1 on p. 121).

  11. 11.

    (Bernays 1930, p. 58) gives the same description of the status of proof theory: Durch die von Ackermann und v. Neumann geführten Beweise ist die Widerspruchsfreiheit für das erste Postulat der Arithmetik, d.h. die Anwendbarkeit des existentialen Schließens auf die ganzen Zahlen sichergestellt. Für das weitere Problem der Widerspruchsfreiheit des Allgemeinbegriffs der Zahlenmenge (bzw. der Zahlenfunktion) einschließlich des zugehörigen Auswahlprinzips liegt ein weitgeführter Ansatz von Ackermann vor.

  12. 12.

    This idea for a syntactic completeness “argument” is made explicit at the end of Gödel’s Königsberg talk (1930c, pp. 26–29). It is connected with the unprovability result he had “recently” proved (to be discussed below in Sect. 5.3). Gödel obtained as a consequence of categoricity and syntactic incompleteness of PM the (semantic) incompleteness of calculi for higher-order logics. – Connections to similar considerations in the Introduction to Gödel’s thesis (Gödel 1929, pp. 60–64) are detailed in (Kennedy 2010).

  13. 13.

    (Hilbert 1928, p. 6). I indicate negations by prefixing with ¬instead of by “overlining” as Hilbert does.

  14. 14.

    See Gödel’s Collected Works V, p. 60. The detailed argument for the latter claim can be found in Gödel’s letter of 2 April 1931; it was given in response to Bernays’s letter of 18 January 1931 (ibid., p. 86ff). Bernays discussed (HR) and introduced an extended version, which is formulated in the next paragraph. Gödel’s analysis applies also to that extension. – A clarifying discussion of (HR) and the ω-rule is found in (Feferman 1986) and (Feferman 2003), but also in (Tait 2002, pp. 417–418).

    The translation is slightly modified from that in the Collected Works; here is the German formulation of the infinitary Bernays Rule: Ist A(x1, …, xn) eine (nicht notwendig rekursive) Formel, in welcher als freie Individuenvariablen nur x1, …, xn auftreten und welche bei der Einsetzung von irgendwelchen Zahlwerten anstelle von x1, …, x n in eine solche Formel übergeht, die aus den formalen Axiomen und den bereits abgeleiteten Formeln durch die logischen Regeln ableitbar ist, so darf die Formel (x1)…(xn)A(x1, …, xn) zum Bereich der abgeleiteten Formeln hinzugenommen werden.

  15. 15.

    Bernays remarks in his (1930, p. 59): Von der Zahlentheorie, wie sie durch die Peanoschen Axiome, mit Hinzunahme der rekursiven Definition, abgegrenzt wird, glauben wir, daß sie in diesem Sinne deduktiv abgeschlossen ist [i.e., is syntactically complete]; die Aufgabe eines wirklichen Nachweises hierfür ist aber noch völlig ungelöst. Noch schwieriger wird die Frage, wenn wir, über den Bereich der Zahlentheorie hinaus, zu der Analysis und den weiteren mengentheoretischen Begriffsbildungen aufsteigen.

  16. 16.

    Feferman makes exactly this point and conjectures in his Introductory Note to Gödel’s correspondence with Bernays: “Since Hilbert had previously conjectured the completeness of Z, he would have had to have a reason to propose such an extension, and the only obvious one is the incompleteness of Z.” (Feferman 2003, Note l on p. 44) – Z is of course elementary number theory.

  17. 17.

    (Gödel 1931a, p. 203 in Collected Works I). I modified the translation; the German text is: Man kann (unter Voraussetzung der Widerspruchsfreiheit der klassischen Mathematik) sogar Beispiele für Sätze (und zwar solche von der Art des Goldbachschen oder Fermatschen) angeben, die zwar inhaltlich richtig, aber im formalen System der klassischen Mathematik unbeweisbar sind. Fügt man daher die Negation eines solchen Satzes zu den Axiomen der klassischen Mathematik hinzu, so erhält man ein widerspruchsfreies System, in dem ein inhaltlich falscher Satz beweisbar ist. – The background is described in Dawson’s Introductory Note, ibid., pp. 196–199, and in (Dawson 1997, pp. 68–79). – Gödel’s Collected Works III contain the report on his thesis work he gave to the Königsberg Congress (cf. note 9). He remarks after discussing the connection of categoricity and Entscheidungsdefinitheit that his result can be stated as follows: Das Peanosche Axiomensystem mit der Logik der Principia Mathematica als Überbau ist nicht entscheidungsdefinit.

  18. 18.

    (Wang 1981, pp. 654–655). Parsons’s Introductory Note to the correspondence with Wang in Gödel’s CollectedWorks describes in Sect. ?? the interaction between Gödel and Wang on which Wang’s paper was based. – There are some seeming oddities with this and related other accounts: (i) Gödel parenthetically seems to claim in the published transcript (1931a) that the undecidable statement is of a restricted number theoretic form; that would be in striking conflict with his own account in (Wang 1981). However, it is only claimed that the statement is universal with a finitist matrix. Indeed, in the Nachtrag Gödel specifies, fully in accord with the report in (Wang 1981), the purely arithmetic character of the undecidable sentence. (ii) Carnap reports from an August 1930 meeting with Gödel that the latter had pointed out undecidability, but also “difficulty with consistency”. That has been taken as an indication that Gödel had a version of his second theorem already then. Such an assumption is in direct conflict with the Gödel-Wang account described above; it receives a convincing explanation through Gödel’s description in (l.c., p. 654), how he found the result, namely, when running into difficulties in his attempt of proving the consistency of analysis.

  19. 19.

    Oystein Ore attended the meeting of the Society of German Scientists and Physicians and reports in (Reid 1970, p. 195), “I remember that there was a feeling of excitement and interest both in Hilbert’s lecture and in the lecture of von Neumann on the foundations of set theory – a feeling that one now finally was coming to grips with both the axiomatic foundation of mathematics and with the reasons for the applications of mathematics in the natural sciences.” Dawson reports that Gödel left Königsberg only on 9 September, and he speculates that “it is very likely that he [Gödel] was in the audience” when Hilbert presented his lecture (l.c., p. 71).

  20. 20.

    That seems to be in conflict with (Bernays 1935, p. 215): “Noch ehe dieses Gödelsche Resultat bekannt war, hatte Hilbert die ursprüngliche Form seines Vollständigkeitsproblems bereits aufgegeben. In seinem Vortrag Die Grundlegung der elementaren Zahlenlehre [i.e., (Hilbert 1931a)] behandelte er dieses Problem für den Spezialfall von Formeln der Gestalt (x)A(x), welche außer x keine gebundene Variable enthalten.” The question is of course not, why did Hilbert give up on the form of that problem(which he did not), but rather, why did he give up on the completeness conjecture? – In Bernays’s correspondence with Gödel (Gödel’s Collected WorksIV, p. 84) there is a peculiar and uncharacteristic lack of familiarity with Hilbert’s Hamburg talk. Bernays attributes the insight – “Die Widerspruchsfreiheit der neuen Regel folgt aus der Methode des Ackermannschen (oder auch des v. Neumannschen) Nachweises für die Widerspruchsfreiheit von Z.” – to an observation of A. Schmidt, when Hilbert’s consistency proof for the new rule is explicitly an extension of Ackermann’s proof (as discussed above in Sect. 5.2)!

  21. 21.

    BernaysNachlass at the ETH Zürich, Hs 975: 4123. See also (Mancosu 1999b, p. 33). Like Mancosu I thank Bernd Buldt for pointing me to this letter.

  22. 22.

    (Hilbert* 1917, p. 40). The German text is: Haben wir gewisse Sätze vor uns, über deren Richtigkeit wir nichts Sicheres aussagen können, so greifen wir einige, die uns eine ausgezeichnete Rolle zu spielen scheinen, als ein vorläufiges Axiomsystem heraus – sei es dass wir die Einfachsten unter ihnen wählen, sei es dass wir diejenigen bevorzugen, die uns am sichersten fundiert oder auch am anschaulichsten erscheinen.

    The German text of the following sentence is: Ist wirklich das gesamte vorliegende Tatsachenmaterial die logische Folgerung aus den herausgegriffenen besonderen Sätzen, die wir als Axiome dem System zu Grunde gelegt haben?

  23. 23.

    (von Neumann 1931, p. 118). The German text is: Es ist ein Konstruktionsverfahren anzugeben, das sukzessiv alle Formeln herzustellen gestattet, welche den “beweisbaren” Behauptungen der klassischen Mathematik entsprechen. Dieses Verfahren heiße darum “Beweisen”.

  24. 24.

    The insight that syntactic completeness and decidability amounted to the same thing had to wait for the mathematical characterization of “formal” theories and decidability. Bernays discusses in his (1930) syntactic completeness and adds on p. 59 in note 19 the remark: Man beachte, daß die Forderung der deduktiven Abgeschlossenheit [i.e., syntactic completeness, WS] noch nicht so weit geht wie die Forderung der Entscheidbarkeit einer jeden Frage der Theorie, welche besagt, daß es ein Verfahren geben soll, um von jedem beliebig vorgelegten Paar zweier der Theorie angehöriger, einander kontradiktorisch entgegengesetzter Behauptungen zu entscheiden, welche von beiden beweisbar (“richtig”) ist.

  25. 25.

    Gödel’s first two letters to von Neumann have not been preserved, it seems. The core content of the letters can be inferred from von Neumann’s responses and from Gödel’s discussion of von Neumann’s perspective at the meeting of the Vienna Circle of 15 January 1931. In (Dawson 1997, p. 70) one finds Hempel’s report on the course in proof theory he took with von Neumann in Berlin during the winter term 1930–1931: “… in the middle of the course von Neumann came in one day and announced that he had just received a paper from a young mathematician in Vienna … who showed that the objectives which Hilbert had in mind … could not be achieved at all.” In a letter of 3 December 1930 to his friend Chevalley, Herbrand writes about the same period: “… I have been here for two weeks, and every time I have seen von Neumann we talk about the work of a certain Gödel, who has produced very curious functions; and all of this has destroyed some quite solidly anchored ideas.”(Details concerning this letter are found in the Appendix of (Sieg 1994).)

  26. 26.

    The letters I refer to in the following are all contained in volume IV of Gödel’s Collected Works. The longer excerpts in this paragraph are found on p. 80, respectively on p. 82.

  27. 27.

    Here and below are some important factual questions. When and where did Bernays learn this from Courant and Schur? How had they been informed? What did Bernays do in the winter term 1930–1931? (It seems that he attended neither the Königsberg meeting nor the lecture Hilbert gave in December 1930 in Hamburg.) We know that Gentzen spent this very term in Berlin; did he attend von Neumann’s lectures? Did he have contact there with Bernays and Herbrand? (Cf. Note 22.) - As to the latter question, Menzler-Trott is “convinced” that Gentzen talked with all three (Bernays, Herbrand, and von Neumann) while in Berlin. In the same note of 7 December 2010 in which he expressed this conviction about Gentzen, Menzler-Trott reports that Bernays participated in 1930/1931 in the meetings of the Berliner Gesellschaft für empirische Philosophie with, among others, Dubislav, Grelling, Hempel, and Reichenbach. It may very well be that Bernays learned here about Gödel’s Königsberg result, as Dubislav participated in that meeting and Hempel heard about it in von Neumann’s lecture. (Cf. Note 22.) – The name of the Berliner Gesellschaft was changed in 1931, as suggested by Hilbert, to Berliner Gesellschaft für wissenschaftliche Philosophie.

  28. 28.

    (Gödel’s Collected Works IV, p. 104). It is mentioned in (Hilbert and Bernays 1934, p. 422), that nested recursions are formalizable in arithmetic and that Gödel and von Neumann discovered this fact.

  29. 29.

    In his letter of 15 November 1932 to Heyting, Gödel remarks somewhat indignantly: Bernays hat in seinem Züricher Vortrag (soviel mir bekannt) auch zugegeben, daß man die Widerspruchsfreiheit d[er] Zahlentheorie bisher nur mit einer von Herbrand gegebenen Einschränkung für die vollständige Induktion beweisen kann. (Gödel’s Collected Works V, p. 60).

  30. 30.

    (Mancosu 1999b, p. 49 and note 14). – The German text of von Neumann’s note is: Übrigens habe ich mich entschlossen, Gödel nicht zu erwähnen, da die Ansicht, dass noch eine gewisse Hoffnung für die Beweistheorie existiert, Vertreter gefunden hat: u[nter] a[nderen] Bernays und Gödel selbst. Zwar ist m[eines] E[rachtens] diese Ansicht irrig, aber eine Diskussion dieser Frage würde aus dem vorliegenden Ra[h]men hinausführen, ich möchte daher bei einer anderen Gelegenheit darüber sprechen.

  31. 31.

    This focus is fully in accord with the earlier considerations, e.g., in Hilbert’s second Hamburg talk of 1927; see p. 471 and p. 479 for consistency, p. 470 and p. 476 for tertium non datur.

  32. 32.

    The negation for general statements is later defined inductively by using classical equivalences; for example, the negation of the conditional A → B is given by A& ¬B, that of (x)A(x) by ( ∃x) ¬A(x). – In the earlier Hamburg lecture the Axiom des Widerspruchs is the principle (A → (B& ¬B)) →  ¬A. – Note that the law of excluded middle implies tnd via the definition of the negation of a universally quantified statement.

  33. 33.

    The arguments leading to this goal are barely sketched, and some are deeply problematic. Gödel made a critical remark about Hilbert’s paper in a letter to Heyting of 16 May 1933: Ich glaube überhaupt, Sie beurteilen Hilberts letzte Arbeiten etwas zu günstig. Z.B. ist doch in Göttinger Nachr. 1931 [(Hilbert 1931b), WS] kaum irgend etwas bewiesen. – In conversation with Olga Taussky-Todd, so it is reported in (Taussky-Todd 1987, p. 40), Gödel “lashed out against Hilbert’s paper [(1931b), WS], saying something like ‘how can he write such a paper after what I have done?’ Hilbert in fact did not only write this paper in a style irritating Gödel, he gave lectures about it in Göttingen in 1932 and other places.”

    It is worth noting that (Hilbert 1931b) was neither reprinted in Hilbert’s Gesammelte Abhandlungen nor mentioned in (Bernays 1935). In contrast, Bernays’s paper discusses (Hilbert 1931a) on pp. 215–216: Das Verfahren, durch welches hier Hilbert die positive Lösung des Vollständigkeitsproblems (für den von ihm betrachteten Spezialfall) sozusagen erzwingt, bedeutet ein Abgehen von dem vorherigen Programm der Beweistheorie. In der Tat wird ja durch die Einführung der zusätzlichen Schlußregel die Forderung einer restlosen Formalisierung der Schlüsse fallen gelassen.

    In his contribution to the Encyclopedia of Philosophy, Bernays mentions both papers and remarks summarily after a brief discussion of Gentzen’s consistency proof: “The broadened methods [of Gentzen, WS] also permitted a loosening of the requirements of formalizing. One step in this direction, made by Hilbert himself, was to replace the schema of complete induction by the stronger rule later called infinite induction …” (p. 502) – On my reading of (Hilbert 1931b) there is no infinite rule in the system, but rather a finitistically justified introduction of universally quantified statements using (HR  ∗ ). (Indeed, Hilbert’s proof that the system expanded by tnd is consistent exploits the finiteness of proof figures; see the discussion below.)

  34. 34.

    Hilbert argues simultaneously for the correctness of these instances of the law of excluded middle by an inductive argument on the complexity of the formulae in the instances of tnd used in the proof. It is difficult to see, why the matrix A(ai) should be of the appropriate form (y)B(y, ai) to allow the formulation of tnd and its use in the induction hypothesis. – Note that Hilbert does not mention a necessary modification in the upper part of the derivation in case axioms of the form (2) are actually used to infer A(ai) via modus ponens with (x)A(x) as the minor premise. All the instances A(ai) must be inferred from (x)A(x) and formed into a conjunction – before carrying out modus ponens … to infer the A(ai). Gentzen will avoid for intuitionist logic such odd detours through the natural deduction formulation of the logical principles and his normalization proof!

  35. 35.

    (Cod. Ms. D. Hilbert 21, 5). The German text is: Was die Beziehung zu Ihrer letzten Note betrifft, so kann ja im Vorwort gesagt werden, dass die Ausführungen des Buches sich ausschliesslich im Rahmen des finiten Standpunktes bewegen (d.h. anderweitige Betrachtungen werden höchstens im heuristischen Sinne angestellt), dass daher Ihre letzte Note, die einen anderen methodischen Standpunkt zugrundelege, nicht in den Bereich dieser Betrachtungen falle. Bernays continues: Auch im Rahmen des finiten Standpunktes wird ja einiges noch ausserhalb bleiben, dessen Behandlung in einem “2. Teil” ja am Schluss des Textes angekündigt, bezw. in Aussicht genommen werden kann; nämlich, 1. die Formalisierung der “zweiten Stufe” (εf), 2. die Formalisierung der Metamathematik (Resultate von Gödel).

  36. 36.

    This connection is never far from Hilbert’s considerations as is obvious from his publications. In the manuscript SUB 603 one finds this remark made in a somewhat obscure context in which tertium non datur is discussed: Hiermit ist gezeigt, dass man so schliessen darf. Es ist in der Tat ein Unterschied, ob man hier Schluss mit tertium non datur anwendet oder nicht; v[er]gl[eiche] meine Beweise der Endlichkeit i[n] d[er] Invariantentheorie.

  37. 37.

    For more details concerning Gentzen’s manuscript, see (von Plato 2009, Sect. 5.5); that section is entitled A newly discovered proof of normalization by Gentzen. – The dating of this summary is a conjecture of mine that is supported by three facts: (i) all the results described in Parts I through III have been obtained already (and Part IV for a significant sub-calculus), (ii) the detailed normalization of intuitionist derivations (as indicated most clearly in the longer quotation – at the very end of Sect. 5.6 below – that begins with “Some thought”) is not being pursued, and (iii) Part V articulates the consistency problem still in the manner of (Hilbert 1931b). The consistency problem as formulated here would naturally be dealt with by detailed semantic considerations – and Gentzen began in October 1932 to write detailed, reflective notes on his approach to the problems he was facing in the manuscript INH discussed below.

  38. 38.

    The reference is, I assume, to (Heyting 1930) and to (Glivenko 1929); in the paper (Gentzen 1933) that derives from Part III of the Urdissertation, Heyting is mentioned, but oddly enough Glivenko is not.

  39. 39.

    The German is: Die Widerspruchsfreiheit der Arithmetik wird bewiesen; dabei wird der Begriff der unendlichen Folge von natürlichen Zahlen benutzt, ferner an einer Stelle der Satz vom ausgeschlossenen Dritten. Der Beweis ist also nicht intuitionistisch. Vielleicht lässt sich das tertium non datur wegschaffen.

  40. 40.

    The first two parts are adapted from the lectures on set theory Hilbert gave in the summer term of 1917, (Hilbert* 1917). It would be of interest to examine Hilbert’s possibly modified perspective on set theory. What is also of interest is Hilbert’s discussion of ordinals, in particular ordinals less than ε0.

  41. 41.

    In (Gentzen 1936, p. 513) derivations are defined as sequences of (one-sided) sequents; the transformation into, essentially, tree form is made on p. 542 for the very same reason Hilbert and Bernays made it in 1922, namely, to insure that every sequent, except for the endsequent of course, is used at most once as a premise. Gentzen employed this technique also in the very first step of his relative consistency proof for classical arithmetic when transforming classical into intuitionist proofs, cf. (Gentzen 1933, pp. 126–127, section 4.21). – I mention these matters here, as they seem to answer convincingly, how Gentzen learned about the tree representation of proofs. Von Plato views the issue in a different way. In his (2010) he claims, already in the abstract, “the central component in Gentzen’s work on logical calculi was the use of a tree form for derivations.” Later, when comparing Gentzen’s work with Einstein’s in the latter’s annus mirabilis 1905, he writes: “His [Gentzen’s] amazing discovery of natural deduction and sequent calculus in 1932–1933, with its full control over the structure of derivations, followed from the use of a tree form [von Plato’s emphasis; WS] for derivations. That was the new, simple, and right idea.” That idea was prefigured in earlier proof theoretic work; but that fact by no means distracts from the “amazing” character of the insight into the structure of normal proofs, in particular, their subformula property in first-order logic.

  42. 42.

    Here is the German text: Gerhard Gentzen hat sich – von München kommend – am 29. Oktober 1930 unter der Nummer 1335 des 121. Rektorats in die Matrikel der Friedrich-Wilhelms-Universität zu Berlin eingetragen. Er studierte hier bis zum 11. Marz 1931 Mathematik. Ein Abgangszeugnis ist hier leider nicht überliefert, so dass wir keine Aussage darüber treffen können, welche Vorlesungen er bei wem in diesem Semester belegt hat.

  43. 43.

    Majer has explored all the obvious archival issues implicit in this letter and my account above, but without any positive findings. - Here is the German text of Courant’s letter: Verabredungsgemäss berichte ich Ihnen heute über Herrn Gentzen auf Grund seines Seminarvortrages und einer persönlichen Rücksprache mit ihm. Herr Gentzen behandelte in seinem Seminarvortrag ein besonders schwieriges Thema und bewies dabei in der äusseren und in der geistigen Durchdringung des Stoffes eine überlegene Selbständigkeit, die ihn durchaus als den Typus eines wissenschaftlichlich gerichteten Menschen kennzeichnet. Ich habe danach wie nach einer mündlichen Besprechung das Zutrauen, dass Herr Gentzen verhältnismässig leicht promovieren und auch dann weiter wissenschaftlich arbeiten kann. Da offenbar seine inneren Neigungen ihn sehr stark auf diese Bahn drängen, so kann ich mit voller Verantwortung der Studienstiftung den Rat geben, ihm die Promotion zu bewilligen.

  44. 44.

    A longer excerpt from this letter to Kneser is quoted in (von Plato 2009a, p. 670); a translation of the full letter is in (Menzler-Trott, pp. 30–31).

  45. 45.

    In (Gentzen 1936, note 17, p. 532), this result is attributed to both Bernays and Gentzen himself: Das im Text genannte Ergebnis wurde etwas später, unabhängig von Gödel, auch von P. Bernays und mir gefunden. (In Note 2 to the publication of the German original, i.e., on p. 119, Gentzen describes very concisely in what way Bernays contributed.) It is not clear with respect to which event “etwas später” is to be understood. Gödel presented his result to Menger’s Colloquium on 28 June 1932. In his letter to Heyting of 16 May 1933, Gödel explicitly claims that his result should have become known in Göttingen shortly after his presentation. – The proof of this result is given and refined in (Hilbert and Bernays 1939); it is presented there tellingly under the heading Eliminierbarkeit des ‘tertium non datur’ für die Untersuchung der Widerspruchsfreiheit des Systems (Z).

  46. 46.

    And as Gentzen explicitly did in his dissertation, (Gentzen 1934, p. 189): Die Einführungen stellen sozusagen die “Definitionen” der betreffenden Zeichen dar, und die Beseitigungen sind letzten Endes nur Konsequenzen hiervon, was sich etwa so ausdrücken läßt: Bei der Beseitigung eines Zeichens darf die betreffende Formel, um deren äußerstes Zeichen es sich handelt, nur “als das benutzt werden, was sie auf Grund der Einführung dieses Zeichens bedeutet”. A few lines below Gentzen continues: Durch Präzisierung dieser Gedanken dürfte es möglich sein, die B (eseitigungs)-Schlüsse auf Grund gewisser Anforderungen als eindeutige Funktionen der zugehörigen E (inführungs)-Schlüsse nachzuweisen.

  47. 47.

    Heyting proved this theorem as Theorem 4.8 in his (1930, p. 52) and remarks in a note that the proof was given in (Glivenko 1929); he emphasizes that it is connected to Brouwer’s “Satz von der Absurdität der Absurdität des Satzes vom ausgeschlossenen Dritten”.

  48. 48.

    Documents in the Hilbert Nachlass contained in the folder SUB 603 indicate that Hilbert must have been informed about these matters by the fall of 1932; pages 44 through 47 on which pertinent remarks are made stem from Druckfahnen (page proofs) dated 15 July 1932. On p. 44, in particular, one finds this remark: Es sei eine Formel vorgelegt. Dann ersetze man A ∨ B durch ¬( ¬A& ¬B), ferner (Ex)A(x) durch ¬(x) ¬A(x), ferner ¬A durch A → 1 ≠ 1. … Wenn dann jene Formel bewiesen ist (Tertium wird zugelassen) dann ist die entstandene Formel inhaltlich richtig. Z.B. (x) ¬A(x) ∨ (Ex)A(x), (x)A(x) ∨ ((x)A(x) → w). [w stands for a contradictory formula; WS.]

  49. 49.

    (Gentzen 1932/1933, p. 9). The German text is: Es bedarf einiger Überlegungen, um einzusehen, dass in der Tat jeweils wieder ein richtiger Beweis entsteht. Ich verzichte auf diese genaue Durchführung, da ich von diesen Tatsachen keinen Gebrauch machen werde, sie vielmehr nur zur Veranschaulichung vorführe.

  50. 50.

    The full title of INH is Die formale Erfassung des Begriffs der inhaltlichen Richtigkeit in der reinen Zahlentheorie, Beziehungen zum Widerspruchsfreiheitsbeweis(The formal characterization of the concept of contentual correctness in pure number theory. Relations to the consistency proof). – The manuscript consists of 36 pages in shorthand; Thiel’s typewritten transcription is 69 pages long.

  51. 51.

    INH, p. 2: Man definiert inhaltliche Richtigkeit so: die mathematischen Axiome sind richtig. A&B ist richtig, wenn A richtig ist und B richtig ist; AvB ist richtig, wenn mindestens eines richtig; Ax, wenn bei jeder Zahleinsetzung für x dies richtig, ebenso (x)Ax; Aa, wenn eine Zahl angegeben werden kann, so daß Aa gilt, ebenso (Ex)Ax; A → B, wenn aus der Richtigkeit von A die von B geschlossen werden kann; ¬A, wenn aus A der Widerspruch geschlossen werden kann. - This is in accord with Hilbert’s intended definition of correctness. I have made some trivial notational changes from Thiel’s transcription for easier comparability, and I separated the clauses for the different connectives by semicolons instead of commas.

  52. 52.

    INH, p. 3: Ich suche Aufklärung über die Fragen: wie unterscheidet sich ein formaler Richtigkeits- bzw. Widerspruchsfreiheitsbeweis von einem inhaltlichen, wieso ist ersterer bei gewissen Schlußweisen nicht einmal mit Hilfe dieser selbst (nach Gödel) möglich, liegt dann ein Brückenschluß vor, wie groß ist dessen Sicherheit, wie sind die Zusammenhänge mit dem Gödelschen Beweis, welche Rolle spielen die mat[hematischen] Axiome?

  53. 53.

    “Purely formal correctness proofs” are understood now in a way that will be sharpened in the next paragraph. – It seems that the difference formulated there between semi-contentual and contentual, respectively, purely formal and formal can be accounted for mostly by the formulation of correctness for numeric statements: if that is done syntactically as below, then the proofs would be semi-contentual and purely formal; if that is done by a semantic evaluation of terms, then they would be contentual and formal. On p. 5 of INH Gentzen calls his definition of “correct” for numeric statements purely formal; the definition specifies that the statement can be obtained syntactically by an immediate derivation from the axioms, what is called Normalbeweis below.

  54. 54.

    INH, p. 8: Der halbinhaltliche Beweis macht eine VJ über eine ziemlich komplizierte Aussage. Diese enthält Ri erg x, und dieses Prädikat wird in komplizierten Fällen immer komplizierter. Formale[r] Beweis macht VJ über Ey. No y & erg x = erg y, eine Aussage zwar auch mit logischen Zeichen, doch von einfacherer Natur, auch bei komplizierteren Fällen. – VJ stands, of course, for Vollständige Induktion.

  55. 55.

    INH, p. 10: Jedenfalls muß doch meines Erachtens irgendein Zusammenhang zwischen dem unformalen Element bei der nicht formalisierbaren Definition der “Richtigkeit” und bei der nicht formalisierbaren transfiniten Induktion bestehen. Da ja anscheinend jede von beiden einen nicht formalisierbaren Widerspruchsfreiheitsbeweis ermöglicht.

  56. 56.

    INH, p. 19: Die Absicht ist: einen vorliegenden Beweis mit numerischem Ergebnis schrittweise zu vereinfachen, bis ein numerischer Beweis für dasselbe Ergebnis dasteht. … Ich möchte mit einer möglichst einfachen Wertung auskommen.

  57. 57.

    INH, p. 23: Jeder Beweis hat einen (transfiniten) Wert. Widerspruchsfreiheit für ein System von Beweisen läßt sich nur zeigen durch einen Beweis von höherem Wert als alle diese. Daher der Satz von Gödel. Dies ist zu beweisen zu versuchen. Dabei die Werte feststellen. Ferner dann, ob es Beweise höheren Wertes und trotzdem größerer Sicherheit gibt.

  58. 58.

    Note that Gentzen uses here for the first time in INH the horseshoe as the symbol for the conditional.

    On the margin, he wrote: Richtiger gesagt: bei & ∀ ∨  ∃sind die finiten Deutungen eben noch fast gleichwertig dem An-sich-sein, bei ⊃ geht das … weniger! – Here is the English translation: More correctly one would say: for & ∀ ∨  ∃the finitist interpretations are still almost the same as those given by the An-sich-Auffassung; for  ⊃  that works less.

    It should be emphasized that Gentzen, in this late part of INH from October 1934, repeatedly refers back to the INH notes from 1932; for example, on pp. 25, 29, 30 he refers back to pp. 17–18 and 19–20, 21–22, 16 and 21, respectively.

  59. 59.

    INH, p. 25: Bei & ∀ ∨  ∃geht er gleichlaufend mit dem halbinhaltlichen Beweis, indem er hier das inhaltliche anerkennt. Bei ⊃ springt er ab und geht über zum formalen Beweis, indem er das inhaltliche ⊃ vermeiden will. Das erweckt den Eindruck: man beginnt mit Halbinhaltlich[em]. Dies wird einem fortschreitend immer unheimlicher, da man offenbar fast genau das schon voraussetzt, was man beweisen will. Bei ⊃ endlich entschließt man sich, abzuspringen und rettet sich ins Formale, wodurch der Beweis kompliziert wird und nachher zu seiner Rettung wieder Hilfsmittel besonderer Art, sagen wir: die Superordnung, benötigt.

  60. 60.

    INH, p. 29: Plan für den III. Abschnitt: erst, nach dem Endlichen, die An-sich-Auffassung im Unendlichen, welche der im Endlichen ganz entspricht. Diese lehnen wir ab. Dann die Entwicklung des intu[itionistischen] Standpunktes mit Worten wie auf INH 21–22. (Evtl. gleich Angabe des Gödelschen Übertragungssatzes.) Dann tiefergehende Kritik, wie noch zu entwickeln.

  61. 61.

    Part III is entitled “Bedenkliche und unbedenkliche Schlußweisen in der reinen Zahlentheorie” and the sections have the headings, “Die Mathematik endlicher Gegenstandsbereiche” (section 7), “Entscheidbare Begriffsbildungen und Aussagen im unendlichen Gegenstandsbereich” (section8), “Die “an-sich”-Auffassung der transfiniten Aussagen” (section 9), “Finite Deutung der Verknüpfungszeichen ∀, &, ∃und ∨ in transfiniten Aussagen” (section 10), and finally, “Die Verknüpfungszeichen  ⊃ and ¬in transfiniten Aussagen; die intuitionistische Grenzziehung” (section 11).

  62. 62.

    INH, p. 29: Weil eben der Unterschied von An-sich und konstruktiv nicht formal erfaßt ist. Eben nur dem Sinn nach bekannt. Und das muß auch so sein, dies ist eben das letzte, außermathematische Fundament.

  63. 63.

    INH, p. 33: Vielleicht liegt doch kein Zirkel vor beim ⊃ , oder richtiger, liegt die Sache so: Auch bei den vorigen Zeichen setzt man eine Art “An-sich”-Sinn schon voraus. Freilich ist dieser irgendwie konstruktiver Art. … auch bei ∀z.B. liegt doch inhaltlich ein “An-sich”-Alle vor. Die Begründung auf das “Bestehen einer [korrekten, WS] Herleitung” scheint doch auch keine wirkliche Begründung zu sein. Kann es ja gar nicht. Die “Korrektheit” setzt eben wieder inhaltliches Wissen über den Sinn des ∀voraus, und dies ist ebenso gut ein “An-sich”-Sinn, wenn man will.

  64. 64.

    INH, p. 33: Wodurch unterscheidet sich das”An-sich”- ∀von dem konstruktiven ∀, obwohl für beide die gleichen Schlußweisen gelten? Und bei ∃? Die konstruktive Deutung führt zurück auf etwas “begrifflich Einfaches”. Bei  ⊃  kann man darüber streiten, ob etwas Einfacheres vorliegt oder nicht. Auch die “Idee der Reduzierbarkeit” ist wichtig.

  65. 65.

    (Gentzen 1936, p. 525). The German text is: Das soll im folgenden § 10 für einen beträchtlichen Teil der transfiniten Aussagen und der zugehörigen Schlußweisen durchgeführt werden. In § 11 behandle ich dann die restlichen Aussageformen und Schlußweisen; dabei stößt die Methode auf Schwierigkeiten, und es zeigt sich die Bedeutung der intuitionistischen (1.8) Grenzziehung zwischen erlaubten und unerlaubten Schlußweisen innerhalb der Zahlentheorie; ferner ergibt sich eine andere, noch engere Grenzziehung als ebenfalls verfechtbar. – On p. 532 Gentzen makes this narrower boundary explicit, namely, no general use of the conditional.

  66. 66.

    “Purely formal” has to be understood here differently from INH, namely, as emphasizing, “informally” so-to-speak, that the proof does not have any real content and does not provide a meaningful reduction.

  67. 67.

    (Gentzen 1936, p. 529). The German text is: Man könnte dann, von diesen Überlegungen ausgehend, einen rein formalen Widerspruchsfreiheitsbeweis für diesen Teil der Zahlentheorie entwickeln. Ein solcher hätte aber nicht viel Wert, denn man müßte in dem Beweis selbst transfinite Aussagen und dieselben zugehörigen Schlußweisen benutzen, die man durch ihn ‘begründen’ will. Der Beweis würde also keine eigentliche Zurückführungbedeuten, wohl aber eineBestätigungdesfinitenCharakters der formalisierten Schlußregeln.Wasaber finitist, darüber müßte man sich zuvor im klaren sein (um dann den Widerspruchsfreiheitsbeweis selbst mit finiten Beweismitteln führen zu können).

  68. 68.

    (Hilbert and Bernays 1939), p. 374. The German text is: Falls diese Perspektive sich bewähren sollte, so würde mit dem Gentzenschen Widerspruchsfreiheitsbeweis ein neuer Abschnitt der Beweistheorie eröffnet.

  69. 69.

    In his (1941), 1941 considers the principle of transfinite induction up to ε0 as non-finitist, but remarks that his position should not be considered “as the standpoint of the Hilbert School”. In the quotation here, but also in other places of his paper, for example on p. 564, Gentzen speaks quite clearly as providing a finitistinterpretation. May that also be in the background for Hilbert’s famous remark in the Preface to the first volume of Grundlagen der Mathematik, that Gödel’s results do not show that proof theory cannot be carried through, but rather that the finitist standpoint has to be exploited in a sharper way in order to obtain consistency proofs for more complex formalisms? – It would be of great biographical interest, but also of significance for our understanding of the systematic proof theoretic developments, if we would know more about the relation between Gentzen and Hilbert, most importantly, during the time from 1931 to 1934, but also after November 1935, when Gentzen had been appointed as Hilbert’s “Special Assistant”. Menzler-Trott conjectures that, during the later period, they only talked about “newspapers, poems and popular science”.

  70. 70.

    This connection remains to be explored; here I point to the summary in Gentzen’s paper, pp. 564–565, and the related discussion in (Sieg & Parsons, pp. 83–85). The most significant connection of Gödel’s to Gentzen’s first consistency proof, revealed in his Zilsel Lecture, has been detailed in (Tait 2005).

  71. 71.

    (Menzler-Trott, p. 55). The more extended text is: “At the moment I am preparing a consistency proof for pure (i.e. no analytic means employed) number theory, which I have finished, for publication in Mathematische Annalen.”

  72. 72.

    (Hilbert 1931b, p. 121). The German text is: Endlich werde noch die wichtige und für unsere Untersuchungen entscheidende Tatsache hervorgehoben, die darin besteht, daß die sämtlichen Axiome und Schlußschemata VI, die ich transfinit genannt habe, doch ihrerseits streng finiten Charakter haben: die in ihnen enthaltenen Vorschriften sind im Endlichen ausführbar.

  73. 73.

    That is in conflict with the earlier perspective on the finitist standpoint. – Even in Über die Grundlagen des Denkens, SUB 604, Hilbert explicitly asserts that the concept “widerspruchsfrei” is “absolut” (on p. 6 of the original manuscript); but that particular use may not be in conflict with the new perspective, as absolute is used here in a different sense: ‘Widerspruchsfrei’ – ebenso wie ‘Richtig’ – ist ein absoluter Begriff; denn wir setzen ausdrücklich fest, dass beim Beweisen als zulässige Begriffs- und Schlussmethoden jedesmal nur diejenigen anzusehen sind, die das Verständnis der Aussage A nötig macht, so dass hinsichtlich der Bedeutung unserer Definitionen von ‘widerspruchsfrei’ und ‘richtig’ keine Unbestimmtheit eintritt.

References

  1. The translations in the text are mine, except when quoted explicitly from particular publications.

    Google Scholar 

  2. Ackermann, W. 1924. Begründung des “tertium non datur” mittels der Hilbertschen Theorie der Widerspruchsfreiheit. Mathematische Annalen 93: 1–36.

    Article  Google Scholar 

  3. Ackermann, W. 1925–1926. Letters to Bernays of 25 June 1925 and 31 March 1926: Wissenschaftshistorische Sammlung, ETH Zürich, Bernays Nachlass, HS 975: 96 and 97.

    Google Scholar 

  4. Ackermann, W. 1940. Zur Widerspruchsfreiheit der Zahlentheorie. Mathematische Annalen 117: 162–194.

    Article  Google Scholar 

  5. Avigad, J., and R. Zach. 2007. The epsilon calculus, Stanford encyclopedia of philosophy (version of July 2007). http://plato.stanford.edu/entries/epsilon-calculus/#6

  6. Benacerraf, P., and H. Putnam (eds.). 1983. Phil osophy of mathematics, 2nd ed. Cambridge: Cambridge University Press.

    Google Scholar 

  7. Bernays, P. 1930. Die Philosophie der Mathematik und die Hilbertsche Beweistheorie. Bliitter für Deutsche Philosophie 4: 326–367. Reprinted in (Bernays 1976, 17–61).

    Google Scholar 

  8. Bernays, P. 1933. Methoden des Nachweises von Widerspruchsfreiheit und ihre Grenzen, in(Saxer 1933, 342–343).

    Google Scholar 

  9. Bernays, P. 1934. ܨber den Platonismus in der Mathematik. Reprinted in (Bernays 1976, 62–78). Trans. in (Benacerraf and Putnam 1983, 258–271).

    Google Scholar 

  10. Bernays, P. 1935. Hilberts Untersuchungen ü ̈ber die Grundlagen der Arithmetik, in (Hilbert 1935, third volume, 196–216).

    Google Scholar 

  11. Bernays, P. 1941. Sur les questions méthodologiques actuelles de la théorie Hilbertienne de la démonstration. In Les entretiens de Zürich sur les fondements et la méthode des sciences mathématiques, ed. F. Gonseth, 144–152. Zurich: Leemann & Co., Discussion, 153–161.

    Google Scholar 

  12. Bernays, P. 1965. Betrachtungen zum Sequenzenkalkül. In Contributions to logic and methodology in honor of J.M. Bochenski, ed. A-T. Tymieniecka and C. Parsons, 1–44. Amsterdam: North-Holland Publishing Company.

    Google Scholar 

  13. Bernays, P. 1967. Hilbert, David. In Encyclopedia of philosophy, vol. 3, ed. P. Edwards, 496–504. New York: Macmillian and Co.

    Google Scholar 

  14. Bernays, P. 1976. Abhandlungen zur Philosophie der Mathematik. Darmstadt: Wissenschaftliche Buchgesellschaft.

    Google Scholar 

  15. Bernays, P. 1977. Three recorded interviews, given on 25.7.1977, 13.8.1977, 27.8.1977. Wissenschaftshistorische Sammlung, ETH Zürich, Bernays Nachlass, Cod. Ms. P. Bernays T 1285.

    Google Scholar 

  16. Coquand, T. 1995. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic 60: 325–337.

    Article  Google Scholar 

  17. Dawson, J. 1986. Introductory note to (Gödel 1931a), in (Gödel 1986, 196–199).

    Google Scholar 

  18. Dawson, J. 1997. Logical dilemmas: The life and work of Kurt Gödel. Wellesley: A. K. Peters.

    Google Scholar 

  19. Ewald, W.B. 1996. From Kant to Hilbert: A source book in the foundations of mathematics, 2 vols. Oxford: Oxford University Press.

    Google Scholar 

  20. Feferman, S. 1986. Introduction to (Gödel 1931b), in (Gödel 1986), 208–213.

    Google Scholar 

  21. Feferman, S. 2003. Introductory note to Gödel’s correspondence with Bernays, in (Gödel 2003a, 41–79).

    Google Scholar 

  22. Feferman, S., and W. Sieg (eds.). 2010. Proofs, categories and computations – Essays in honor of Grigori Mints. London: College Publications.

    Google Scholar 

  23. Gentzen, G. 1932. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen. Mathematische Annalen 107: 329–350.

    Article  Google Scholar 

  24. Gentzen, G. 1932/1933. “Urdissertation”, Wissenschaftshistorische Sammlung, Eidgenössische Technische Hochschule, Zürich, Bernays Nachlass, Ms. ULS. (A detailed description of the manuscript is found in (von Plato 2009a, 675–680)).

    Google Scholar 

  25. Gentzen, G. 1933. Über das Verhältnis zwischen intuitionistischer und klassischer Arithmetik. Archiv für mathematische Logik und Grundlagenforschung 16 (1974): 119–132.

    Article  Google Scholar 

  26. Gentzen, G. 1934/1935. Untersuchungen über das logische Schließen I, II. Mathematische Zeitschrift 39: 176–210, 405–431.

    Google Scholar 

  27. Gentzen, G. 1935. Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie. Archiv für mathematische Logik und Grundlagenforschung 16 (1974): 97–118.

    Google Scholar 

  28. Gentzen, G. 1936. Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen 112: 493–565. Trans. in (Gentzen 1969).

    Google Scholar 

  29. Gentzen, G. 1938. Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. In Forschung zur Logik und zur Grundlegung der exakten Wissenschaften, Neue Folge 4, ed. S. Hirzel, 19–44. Trans. in (Gentzen 1969, 252–286).

    Google Scholar 

  30. Gentzen, G. 1943. Beweisbarkeit und Unbeweisbarkeit von Anfangsfä¨llen der transfiniten Induktion in der reinen Zahlentheorie. Mathematische Annalen 119: 140–161. Trans. in (Gentzen 1969, 287–308).

    Google Scholar 

  31. Gentzen, G. 1969. The collected papers of Gerhard Gentzen. Amsterdam: North-Holland Publishing Company. Edited and translated by M. E. Szabo.

    Google Scholar 

  32. Glivenko, V. 1929. Sur quelques points de la logique de M. Brouwer, Académie Royale de Belgique. Bulletins de la classe des sciences, ser. 5, 15: 183–188.

    Google Scholar 

  33. Gödel, K. 1929. Über die Vollstä ̈ndigkeit des Logikkalkü¨ls, Dissertation, Vienna, in (Gödel 1986, 60–101).

    Google Scholar 

  34. Gödel, K. 1930a. Die Vollständigkeit der Axiome des logischen Funktionenkalküls, in (Gödel 1986), 102–123.

    Google Scholar 

  35. Gödel, K. 1930b. Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit, in (Gödel 1986, 140–143).

    Google Scholar 

  36. Gödel, K. 1930c. Vortrag ü¨ber Vollstä¨ndigkeit des Funktionenkalkü¨ls, in (Godel 1995, 16–29).

    Google Scholar 

  37. Gödel, K. 1931. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, in (Gö¨del 1986, 126–195).

    Google Scholar 

  38. Gödel, K. 1931a. Diskussion zur Grundlegung der Mathematik, in (Gödel 1986, 200–205).

    Google Scholar 

  39. Gödel, K. 1931b. Besprechung von Hilberts Die Grundlegung der elementaren Zahlentheorie. Zentralblatt für Mathematik und ihre Grenzgebiete 1: 260. Reprinted and translated in (Gödel 1986, 212–214).

    Google Scholar 

  40. Gödel, K. 1932. Über Vollständigkeit und Widerspruchsfreiheit, Mathematisches Colloquium, dated 22 January 1931. Ergebnisse eines mathematischen Kolloquiums 3: 12–13. Reprinted and translated in (Gödel 1986, 234–237).

    Google Scholar 

  41. Gödel, K. 1933. Zur intuitionistischen Arithmetik und Zahlentheorie, in (Gödel 1986, 286–295).

    Google Scholar 

  42. Gödel, K. 1938. Vortrag bei Zilsel, in (Gödel 1995, 85–113).

    Google Scholar 

  43. Gödel, K. 1941. In what sense is intuitionistic logic constructive?, in (Gödel 1995, 189–200).

    Google Scholar 

  44. Gödel, K. 1958/1972. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12: 280–287. Revised and expanded as (Gödel 1972). The German original was reprinted and translated in (Gödel 1990, 240–251). The expanded English version is in (ibid., 271–280).

    Google Scholar 

  45. Gödel, K. 1986. Collected works, vol. I. New York: Oxford University Press.

    Google Scholar 

  46. Gödel, K. 1990. Collected works, vol. II. New York: Oxford University Press.

    Google Scholar 

  47. Gödel, K. 1995. Collected works, vol. III. New York: Oxford University Press.

    Google Scholar 

  48. Gödel, K. 2003a. Collected works, vol. IV. New York: Oxford University Press.

    Google Scholar 

  49. Gödel, K. 2003b. Collected works, vol. V. New York: Oxford University Press.

    Google Scholar 

  50. Herbrand, J. 1931. Sur la non-contradiction de l’arithmétique. Crelles Journal fü¨r die reine und angewandte Mathematik 166: 1–8, in (Herbrand 1971, 282–298).

    Google Scholar 

  51. Herbrand, J. 1971. Logical writings, ed. Warren Goldfarb. Cambridge: Harvard University Press.

    Book  Google Scholar 

  52. Hilbert, D. *1917. Mengenlehre. Lecture notes by M. Goeb, MI.

    Google Scholar 

  53. Hilbert, D. *1921/1922. Grundlagender Mathematik. Lecture notes by P. Bernays, MI.

    Google Scholar 

  54. Hilbert, D. 1922. Neubegrü¨ndung der Mathematik. Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universitat 1, 157–177, in (Ewald 1996, 1117–1134).

    Google Scholar 

  55. Hilbert, D. 1923. Die logischen Grundlagen der Mathematik. Mathematische Annalen 88: 151–165, in (Ewald 1996, 1136–1148).

    Google Scholar 

  56. Hilbert, D. 1927. Die Grundlagen der Mathematik. Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universitat 6(1/2), 65–85. Trans. in (van Heijenoort 1967, 464–479).

    Google Scholar 

  57. Hilbert, D. 1928. Probleme der Grundlegung der Mathematik. Mathematische Annalen 102: 1–9. Reprint, with emendations and additions, of paper with the same title, published in Atti del Congresso internazionale dei matematici, Bologna 1928, 135–141.

    Google Scholar 

  58. Hilbert, D. *1929. Mengenlehre, Lecture notes by Lothar Collatz, Staats- und Universitätsbibliothek Hamburg, Signatur: NL Collatz, 82.

    Google Scholar 

  59. Hilbert, D. 1930. Naturerkennen und Logik. Die Naturwissenschaften 18: 959–963. Reprinted in (Hilbert 1935, 378–387). Trans. in (Ewald 1996, 1157–1165).

    Google Scholar 

  60. Hilbert, D. 1931a. Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen 104: 485–494. Partially reprinted in (Hilbert 1935, 192–195). Trans. in (Ewald 1996, 1148–1157).

    Google Scholar 

  61. Hilbert, D. 1931b. Beweis des tertium non datur, Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-physikalische Klasse, 120–125.

    Google Scholar 

  62. Hilbert, D. 1935. Gesammelte Abhandlungen, 3 vols. Berlin: Springer.

    Google Scholar 

  63. Hilbert, D. 2011. David Hilbert’s lectures on the foundations of mathematics and physics, 1891–1933, vol. 3, ed. W.B. Ewald and W. Sieg. Berlin: Springer. To appear.

    Google Scholar 

  64. Hilbert, D., and P. Bernays. 1934. Grundlagen der Mathematik, vol. I. Berlin: Springer. Second edition, 1968, with revisions detailed in foreword by Bernays.

    Google Scholar 

  65. Hilbert, D., and P. Bernays. 1939. Grundlagen der Mathematik. vol. II. Berlin: Springer. Second edition, 1970, with revisions detailed in foreword by Bernays.

    Google Scholar 

  66. Kennedy, J. 2010. Gödel and “Formalism freeness”: Manuscript, February 25, 2010.

    Google Scholar 

  67. Mancosu, P. 1999a. Between Russell and Hilbert: Behmann on the foundations of mathematics. Bulletin of Symbolic Logic 5(3): 303–330.

    Article  Google Scholar 

  68. Mancosu, P. 1999b. Between Vienna and Berlin: The immediate reception of Gödel’s incompleteness theorems. History and Philosophy of Logic 20: 33–45.

    Article  Google Scholar 

  69. Menzler-Trott, E. 2007. Logic’s lost genius – The life of Gerhard Gentzen. Providence/London: American Mathematical Society/London Mathematical Society.

    Google Scholar 

  70. Menzler-Trott, E. 2010. Personal communication, December 7, 2010.

    Google Scholar 

  71. Parsons, C.D. 2003. Introductory note to the Wang correspondence, in (Gödel 2003b, 379–397).

    Google Scholar 

  72. Reid, C. 1971. Hilbert. New York: Springer.

    Google Scholar 

  73. Richardson, R.G.D. 1932. Report on the congress. Bulletin of the AMS 38(11): 769–774.

    Article  Google Scholar 

  74. Saxer, W. (ed.). 1933. Verhandlungen des Internationalen Mathematiker-Kongresses Zü¨rich 1932, II. Band: Sektionsvorträge, Orell Füssli Verlag.

    Google Scholar 

  75. Schröder-Heister, P. 2002. Resolution and the origins of structural reasoning: Early proof-theoretic ideas of Hertz and Gentzen. Bulletin of Symbolic Logic 8: 246–265.

    Article  Google Scholar 

  76. Schütte, K. 1993. Bemerkungen zur Hilbertschen Beweistheorie, ACTA BORUSSICA V, Beiträge zur ost- und westdeutschen Landeskunde 1991–1995.

    Google Scholar 

  77. Sieg, W. 1994. Mechanical procedures and mathematical experience. In Mathematics and mind, ed. A. George, 71–117. Oxford: Oxford University Press.

    Google Scholar 

  78. Sieg, W. 1999. Hilbert’s programs: 1917–1922. Bulletin of Symbolic Logic 5: 1–44.

    Article  Google Scholar 

  79. Sieg, W. 2002. Beyond Hilbert’s reach? In Reading natural philosophy. Essays in the history and philosophy of science and mathematics, ed. D. Malament, 363–405. Chicago: Open Court. Reprinted in Lindström, S., Palmgren, E., Segerberg, K. and Stoltenberg-Hansen, V. (eds.). 2009. Logicism, intuitionism, and formalism: What has become of them?, 449–483. Dordrecht: Springer.

    Google Scholar 

  80. Sieg, W. 2009. Hilbert’s proof theory. In Handbook of the history of logic, ed. D.M. Gabbay and J. Woods, 321–384. Amsterdam: Elsevier.

    Google Scholar 

  81. Sieg, W., and C.D. Parsons. 1995. Introductory note to (Gödel 1938), in (Gödel 1995), 62–84.

    Google Scholar 

  82. Sieg, W., and C. Tapp. 2011. Introduction to the Undated Draft: The “Undated Draft” is a manuscript most likely written in late 1920/early 1921, in (Hilbert 2011).

    Google Scholar 

  83. Skolem, T. 1922. Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre. Trans. in (van Heijenoort 1967, 290–301).

    Google Scholar 

  84. Tait, W.W. 2002. Remarks on finitism. In Reflections on the foundations of mathematics, Lecture notes in logic, vol. 15, ed. W. Sieg, R. Sommers, and C. Talcott, 410–419. Urbana: Association for Symbolic Logic.

    Google Scholar 

  85. Tait, W.W. 2005. Gödel’s reformulation of Gentzen’s first consistency proof of arithmetic. The Bulletin of Symbolic Logic 11: 225–238.

    Article  Google Scholar 

  86. Tait, W.W. 2010. The substitution method revisited, in (Feferman and Sieg 2010, 231–241).

    Google Scholar 

  87. Taussky-Todd, O. 1987. Remembrances of Kurt Gödel. In Gödel-Symposium in Salzburg, 31–41. Naples: Bibliopolis, July 10–12, 1983.

    Google Scholar 

  88. Troelstra, A.S. 1990. Introductory note to (Gödel 1958/1972), in (Gödel 1990, 217–240).

    Google Scholar 

  89. Troelstra, A.S. 1995. Introductory note to (Gödel 1941), in (Gödel 1995, 186–189).

    Google Scholar 

  90. Van Heijenoort, J. (ed.). 1967. From Frege to Gö¨del: A sourcebook of mathematical logic, 1879–1931. Cambridge: Harvard University.

    Google Scholar 

  91. Von Neumann, J. 1927. Zur Hilbertschen Beweistheorie. Reprinted in (von Neumann 1961, 256– 300).

    Google Scholar 

  92. Von Neumann, J. 1931. Die formalistische Grundlegung der Mathematik. Erkenntnis 2: 116–121. Trans. in (Benacerraf and Putnam 1983, 61–65).

    Google Scholar 

  93. Von Neumann, J. 1961. Collected works, vol. I, ed. A.H. Taub. New York: Pergamon.

    Google Scholar 

  94. von Plato, J. 2008. Gentzen’s proof of normalization for natural deduction. The Bulletin of Symbolic Logic 14: 240–257.

    Article  Google Scholar 

  95. von Plato, J. 2009a. Gentzen’s logic. In Handbook of the history of logic, vol. 5, ed. D.M. Gabbay and J. Woods, 667–721. Amsterdam: Elsevier.

    Google Scholar 

  96. von Plato, J. 2009b. Gentzen’s INH: A brief summary of its main ideas: Personal communication, November 24, 2009.

    Google Scholar 

  97. von Plato, J. 2010. Gentzen’s logical calculi: Aspects of a work of genius: Manuscript, to appear.

    Google Scholar 

  98. Wang, H. 1981. Some facts about Kurt Gödel. Journal of Symbolic Logic 46: 653–659.

    Article  Google Scholar 

  99. Zach, R. 2003. The practice of finitism: Epsilon calculus and consistency proofs in Hilbert’s program. Synthese 137: 211–259.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, 15213, USA

    Wilfried Sieg

Authors
  1. Wilfried Sieg
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wilfried Sieg .

Editor information

Editors and Affiliations

  1. Goteborg, 412 96, Sweden

    P. Dybjer

  2. Dept. Philosophy & Linguistics, University of Umea, Umea, 901 87, Sweden

    Sten Lindström

  3. Dept. Mathematics, Uppsala University, Uppsala, Sweden

    Erik Palmgren

  4. M. de Vrieshof 4, Leiden, 2300 RA, Netherlands

    G. Sundholm

Additional information

Dedicated to Per Martin-Löf.

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer Science+Business Media Dordrecht.

About this chapter

Cite this chapter

Sieg, W. (2012). In the Shadow of Incompleteness: Hilbert and Gentzen. In: Dybjer, P., Lindström, S., Palmgren, E., Sundholm, G. (eds) Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science, vol 27. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-4435-6_5

Download citation

Publish with us

Policies and ethics

Search

Navigation