A Most Interesting, but Revoked Draft for Hilbert and Bernays' "Grundlagen der Mathematik" that never found its way into any publication, and 2 CV of Gisbert Hasenjaeger

TL;DR

This paper investigates a previously unknown draft related to Hilbert and Bernays' foundational work in mathematics, revealing its connection to Hasenjaeger's contributions and the impact of proof theory developments on the text's revision.

Contribution

It uncovers and analyzes a lost draft of Hilbert-Bernays' Grundlagen der Mathematik and documents the collaborative work of Hasenjaeger and Bernays on the second edition.

Findings

Identified a candidate for the revoked draft in Bernays' legacy archive.

Provided evidence linking the draft to Hasenjaeger and Bernays' revision efforts.

Suggested the draft involved a complete reorganization of the first volume.

Abstract

In 1934, in Bernays preface to the 1st edn. of the 1st vol. of Hilbert-Bernays "Grundlagen der Mathematik", a nearly completed draft of the the finally two-volume monograph is mentioned, which had to be revoked because of the completely changed situation in the area of proof theory after Herbrand and Goedels revolutionary results. Nothing at all seems to be known about this draft and its whereabouts. A third of a century later, Bernays preface to the 2nd edn. (1968) of the 1st vol. of Hilbert-Bernays mentions joint work of Hasenjaeger and Bernays on the second edition. Bernays states there that it became obvious that the integration of the many new results in the area of proof theory would have required a complete reorganization of the book, i.e. that the inclusion of the intermediately found new results in the area of proof theory turned out to be unobtainable by a revision, but would have required a complete reorganization of the entire textbook. We document that - even after the need for a complete reorganization had become obvious - this joint work went on to a considerable extent. Moreover, we document when Hasenjaeger stayed in Zurich to assist Bernays in the completion of the 2nd edn. In May 2017, we identified an incorrectly filed text in Bernays scientific legacy at the archive of the ETH Zurich as a candidate for the beginning of the revoked draft for the 1st edn. or of a revoked draft for the 2nd edn. In a partial presentation and careful investigation of this text we gather only some minor evidence that this text is the beginning of the nearly completed draft of the 1st edn., but ample evidence that this text is part of the work of Hasenjaeger and Bernays on the 2nd edn. We provide some evidence that this work has covered a complete reorganization of the entire 1st vol., including a completely new version of its last chapter on the iota.

Full text

A third of a century later, \bernaysplain’ preface to the second edition (1968) of the first volume of \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex” mentions joint workof Hasenjaeger and \bernaysplain on the second edition.  \bernaysplain states there that“it became obvious that the integration of the many new results in the area of proof theory would have required a complete reorganization of the book”,    i.e. that the inclusion of the intermediately found new results in the area of proof theory turned out to be unobtainable by a revision, but would have required a complete reorganization of the entire textbook.  We will document that — even after the need for a complete reorganization had become obvious — this joint work went on to a considerable extent.  Moreover,  we will document when Hasenjaeger stayed in Zurich* to assist \bernaysplain in the completion of the second edition.

In May 2017,  we identified an incorrectly filed text in \bernaysplain’ scientific legacy at the archive of the ETH Zurich as a candidate for the beginning of the revoked draft for the first edition or of a revoked draft for the second edition. In a partial presentation* and careful investigation* of this text we gather only some minor evidence that this text is the beginning of the nearly completed draft of the first edition, but ample evidence that this text is part of the work of Hasenjaeger and \bernaysplain on the second edition. We provide some evidence that this work has covered a complete reorganization of the entire first volume, including a completely new version of its last chapter on the $\iota$.

Contents

@starttoc

toc

1 Introduction

1.1 \hilbertplain–\bernaysplain in general

By the 1930s, ground-breaking work had been achieved by German scientists, especially in philosophy, psychology, physics, chemistry, and mathematics. With the Nazis’ seizure of power in 1933, the historical tradition of German research was discontinued in most areas, and, as a further consequence, many achievements of German science in the first half of the 20 th century have still not been sufficiently recognized. This is the case especially for those developments that had not been completed before the Nazis covered Germany under twelve years of intellectual darkness.

David \hilbertplain (1862–1943) is one of the most outstanding representatives of mathematics, mathematical physics, and logic-oriented foundational sciences in general [Reid, 1970].  From the end of the 19 th century to the erosion of the University of G*ottingen by the Nazis,  \hilbertplain formed and reshaped many areas of applied and pure mathematics.  Most well-known and highly acknowledged are his “Foundations of Geometry”  [Hilbert, 1899].

After initial work at the very beginning of the 20 th century,  \hilbertplain re-intensified his research into the logical foundations of mathematics in  1917,  together with his new assistant Paul  \bernaysplain (1888–1977).   Supported by their PhD student Wilhelm Ackermann (1896–1962),  \bernaysplain  and \hilbertplain developed the field of proof theory (or metamathematics), where formalized mathematical proofs become themselves the objects of mathematical operations and investigations — just as numbers are the objects of number theory.  The goal of \hilbertplain’s endeavors in this field was to prove the consistency of the customary methods in mathematics once and for all, without the loss of essential theorems as in the competing intuitionist movements of Kronecker, Brouwer, Weyl, and Heyting.  The proof of the consistency of mathematics was to be achieved by sub-division into the following three tasks:

• •

Arithmetization of mathematics.

• •

Logical formalization of arithmetic.

• •

Consistency proof in the form of a proof of impossibility:  It cannot occur in arithmetic that there are formal derivations of a formula $A$ and also of its negation $\rule{0.0pt}{10.33327pt}{\overline{A}}.$

The problematic step in this program (nowadays called \hilbertplain*’Ŋ program*)  is the consistency proof.

\hilbertplain’Ŋ program was nourished by the hope that mathematics — as the foundation of natural sciences, and especially of modern physics — could thus provide the proof of its own groundedness. This was a paramount task of the time, not least because of the foundational crisis in mathematics (which had been evoked among others by Russell’Ŋ Paradox at the beginning of the 20 th century)  and the vivid philosophic discussions of the formal sciences stimulated inter alia by Wittgenstein and the Vienna Circle.111 Cf. e.g. [Wittgenstein, 1994], [Waismann, 1967].

It should be recognized that \hilbertplain’s primary goal was neither a reduction of mathematical reasoning and writing to formal logic as in the seminal work of ? [Whitehead & Russell, 1910–1913],  nor a formalization of larger parts of mathematics as in the publications of the famous French ? [Bourbaki, 1939ff.]  group of mathematicians.   His ambition was to secure — once and for all — the foundation of mathematics with consistency proofs, in which an intuitively consistent, “finitist” part of mathematics was to be used for showing that no contradiction could be formally derived in larger and larger parts of non-constructive and axiomatic mathematics.

\hilbertplain’Ŋ program fascinated an elite of young outstanding mathematicians, among them John von Neumann (1903–1957),  Kurt  G*odel (1906–1978),  JacqueŊ Herbrand (1908–1931),  and Gerhard Gentzen (1909–1945),  whose contributions essentially shaped the fields of modern mathematical logic and proof theory.

We know today that \hilbertplain’s quest to establish a foundation for the whole scientific edifice could not be successful to the proposed extent:  G*odel’s incompleteness theorems dashed the broader hopes of \hilbertplain’Ŋ program. Without the emphasis that \hilbertplain has put on the foundational issues, however, our negative and positive knowledge on the possibility of a logical grounding of mathematics (and thus of all exact sciences) would hardly have been achieved at his time.

1.2 Drafts for \hilbertplain–\bernaysplain

The central and most involved presentation of \hilbertplain’Ŋ program and \hilbertplain’s proof theory is found in the two-volume monograph “\grundlagendermathematiknoindex” of ? [?; ?], and its second revised edition [?, ?; ?].

We should not forget the historical context of the original writing of these texts in the late 1920s and the 1930s:   First, Herbrand’Ŋ Fundamental Theorem and Godel’s incompleteness theorems hit the new field of proof theory like a hurricane.  Moreover, after the Nazi takeover of Germany in January 1933,  \bernaysplain was expelled from his academic position in Gottingen in April 1933,  and had to leave the country.  As a consequence, both volumes show strong signs of reorganization and rewriting, sometimes even the signs of hurry to meet the publication deadlines.

Because of this editorial and historical context, the drafts for both editions of the two \hilbertplain–\bernaysplain volumes are of special interest, in particular the drafts that did not find their way into any of the editions.

Until recently, however, we did not know anything substantial about these revoked drafts for \hilbertplain–\bernaysplain.  In May 2017, however, we identified an incorrectly filed text in \bernaysplain’ scientific legacy in the archive of the ETH Zurich as a candidate for such a revoked draft.  We will describe and investigate this text in this paper, and discuss at what time it was probably written, and by whom, \etc

There are two infamous revoked drafts for \hilbertplain–\bernaysplain of which \bernaysplain stated that they at least had existed — one for the first and one for the second edition:

1.2.1 The Mentioning of the Draft for the First Edition

\bernaysplain

’ “Vorwort zur erŊten Auf lage” (“Preface to the First Edition”)  of [Hilbert & Bernays, 1934, p.VII f.],  begins as follows:

“Eine Darstellung der BeweiŊtheorie, welche auŊ dem \hilbertplainschen Ansatz zur Behandlung der mathematisch-logischen Grundlagenprobleme erwachsen ist, wurde schon seit langerem von \hilbertplain angekundigt.

Die AuŊfuhrung dieseŊ VorhabenŊ hat eine wesentliche Verzogerung dadurch erfahren, daȷ in einem Stadium, in dem die Darstellung schon ihrem Abschluȷ nahe war, durch daŊ Erscheinen der Arbeiten von Herbrand und Godel eine veranderte Situation im Gebiet der BeweiŊtheorie entstand, welche die Berucksichtigung neuer Einsichten | zur Auf gabe machte. Dabei ist der Umfang deŊ BucheŊ angewachsen, so daȷ eine Teilung in zwei Bande angezeigt erschien.”

In the translation of  [Hilbert & Bernays, 2017a, p.VII.b, engl.]  (comments omitted):

“Some time ago, \hilbertplain announced a presentation of the proof theory that developed from the \hilbertplainian approach to the problems in the foundations of mathematics and logic.

The execution of this enterprise received considerable delay because the whole field of proof theory was changed by the publication of the works of Herbrand and G*odel when our work was already close to completion;  and this change put the consideration of new insights | onto the agenda.  As a consequence of this, the size of the book grew to the extent that a separation into two volumes seemed appropriate.

Nothing about this work “already close to completion” and its whereabouts seems to be known.

1.2.2 The Mentioning of the Given-Up Work on the Second Edition

\bernaysplain

’ “Vorwort zur zweiten Auf lage” (“Preface to the Second Edition”)  of  [Hilbert & Bernays, 1968, p.V]  begins as follows:

“Schon vor etlichen Jahren haben der verstorbene Heinrich Scholz  und Herr F. K. Schmidt  mir vorgeschlagen, eine zweite Auf lage der “\grundlagendermathematiknoindex” vorzunehmen, und Herr G. Hasenjaeger  war auch zu meiner Unterstutzung bei dieser Arbeit auf einige Zeit nach Zurich gekommen.  EŊ zeigte sich jedoch bereitŊ damalŊ, daȷ eine Einarbeitung der vielen im Gebiet der BeweiŊtheorie hinzugekommenen Ergebnisse eine vollige Umgestaltung deŊ BucheŊ erfordert hatte.  Erst recht kann bei der jetzt vorliegenden zweiten Auf lage, zu der wiederum Herr F. K. Schmidt den Anstoȷ gab, nicht davon die Rede sein, den Inhalt dessen, waŊ seither in der BeweiŊtheorie erreicht worden ist, zur Darstellung zu bringen.”

In the translation of  [Hilbert & Bernays, 2017a, p.V, engl.]:

“A number of years ago, the late Heinrich Scholz and Mr. F. K. Schmidt suggested the undertaking of a second edition of the “Foundations of Mathematics”;  and moreover, to assist me in this work, Mr. G. Hasenjaeger came to Z*urich for some time.  Already back then, it became obvious that the integration of the many new results in the area of proof theory would have required a complete reorganization of the book.  Furthermore, the present second edition (the impetus for which came again from Mr. F. K. Schmidt)  can by no means present the substance of the achievements in proof theory since the appearance of the first edition.”

In \sectrefsection Joint Work,  we will document when \hasenjaegernameplain came to Zurich for this purpose, and provide some evidence that the work of Hasenjaeger and \bernaysplain has covered a complete reorganization of the entire first volume,  which means that the main document of this collaboration and its whereabouts still remain completely unknown,  and also that \bernaysplain may give us a wrong impression by using the subjunctive “erfordert hatte” (“would have required”) in the above quotation.

2 Our Typescript

The unpublished typescript we discuss in this paper will briefly be called “our typescript”.

2.1 Form, Location, and Incorrect Filing of Our Typescript

Its outer form is as follows:  It is an untitled typescript, with corrections by \bernaysplain’ hand.  Our typescript has 34 pages, with page numbers 2–34 on the respective page headers.  Its spelling is German–Austrian, and it includes the German letter “ȷ” not found on typewriters with Swiss layout.  In this context it may be relevant that — according Ludwig \bernaysplain [Bernays, 2017] — his close uncle and legator Paul  \bernaysplain never had a typewriter and is not known to have ever used one.

The location of our typescript is the archive (ETH-Bibliothek, Hochschularchiv) of the ETH Zurich (Swiss Federal Institute of Technology in Z*urich) (Switzerland).

The folder in which our typescript was found there by \wirthnamenoindex on May 12, 2017,  was one of two folders in the legacy of Paul  \bernaysplain under the label “Hs 973: 41”,   which is listed in the inventory [Bernays, 1986]  on page 7 as

“41.  Texte und Korrekturen zur Neuauf lage deŊ “GrundlagenbucheŊ” Bd. II von David \hilbertplain und Paul  \bernaysplain. 1970    2 Mappen”

In English:

“41.  Texts and corrections for the new edition of the “Foundations Book” Vol. II by David \hilbertplain und Paul  \bernaysplain. 1970    2 folders”

This is a wrong place for our typescript because its contents refer exclusively to Vol. I,  published in 1934 (1 st edn.) and in 1968 (2 nd edn.)  —  neither to Vol. II,  nor to the year 1970.  Thus, regarding its subject, our typescript was incorrectly filed, and probably still is.

2.2 Two Additional Copies of  Our Typescript, With Footnotes!

Moreover, in January 2018, in the legacy of \hasenjaegernameplain,222By the end of the year 2018, Beate Becker gave her part of the scientific legacy of her father \hasenjaegernameplain in 9 boxes to the following archive: Legacy of \hasenjaegernameplain, Deutsche Museum, Munchen, Archiv: “Nachlasse H, NL 288”. his daughter Beate Becker succeeded in finding two carbon copies of our typescript.

Both of these carbon copies come without the corrections by \bernaysplain’ hand found in our typescript,  but one of them has most of these corrections added (mostly with a typewriter),  and the other includes the typewriting of even more of the corrections by \bernaysplain’ hand found in our typescript.

One of these carbon copies comes with two extra typewritten pages containing all footnotes for our typescript, again corrected by \bernaysplain’ hand.  Our typescript, however, does not contain any footnotes at all, but only raised closing parentheses (without any numbers, letters, asterisks or other signs) to indicate their respective positions in the text.

Regarding the font and the actual typing of the letters, we did not find any differences between our typescript and the extra footnote pages found by Beate Becker.

2.3 Presentational Form of Our Excerpts

The deletions and additions by \bernaysplain’ handwritten remarks are not documented in the following excerpts from our typescript;  only the version of our typescript after the application of \bernaysplain’ hand-written corrections is presented here.

Therefore, the rare deletions (this text is deleted)  and additions ([this text is added])  indicated in these excerpts are ours, not \bernaysplain.’

Moreover — in these excerpts — the footnotes of the form […] are our additions, whereas the other footnotes are those from the two extra pages found with one of the two carbon copies of our typescript in the Hasenjaeger legacy (cf. \sectrefsection carbon copies).

All footnote numbers in these excerpts are introduced by us.  This form of presentation seems appropriate in particular because our typescript has no footnotes (but only raised closing parentheses to indicate their positions, cf. \sectrefsection carbon copies).

The positions of the original page breaks in our typescript are indicated by the sign “|” in our excerpts, with the number of the new page in a lower index, i.e. “|5” for the page break from page 4 to page 5.

2.4 Discussion and Excerpts

of  ď 1 of  Our Typescript

The first section of our typescript has the headline “Einleitung.” (“Introduction.”)  and the additional subsection headline  “ď 1. Einf*uhrung in die Fragestellung” (“ď 1. Introduction to the Problem Definition”).

2.4.1 Parallel introductory part, several paragraphs missing in our typescript

The text starts literally with the first paragraph of  ď 1 of [?, ?; ?] (p. 1),  including the enumerated list of three items.

The next paragraph of [?, ?; ?],  however,  is not present in our typescript,  namely the paragraph on the “versch*arften methodischen Anforderungen” (“sharpened methodological requirements”) resulting in “eine neue Art der AuŊeinandersetzung mit dem Problem deŊ Unendlichen” (“to deal with the problem of the infinite in a new way”).

Then, however, the text continues almost literally with the penultimate paragraph and the first sentence of the last paragraph of  p. 1 of [?, ?; ?].   The part on the subject of the “exiŊtentiale Form” (“existential form”) (which starts in the middle of the last paragraph of  p. 1 and runs up to the end of the 1 st paragraph starting on p. 2)  is again missing in our typescript – just as the introduction to this subject was omitted before, namely in the paragraph on “the problem of the infinite”,   right after the enumerated list of three items.  Instead of this part, the paragraph ends in our typescript with a digression into satisfiability and consistency.

Then the last paragraph on p. 2 of our typescript follows almost literally the text from the 2 nd paragraph starting on p. 2 of  [?, ?; ?]  up to the end of the 2 nd paragraph starting on p. 3 of  [?, ?; ?],  where only the last part of the last sentence

“alŊ g*ultig vorauŊgesetzt, und wir kommen so zu der Frage, welcher Art diese Geltung ist.”

“presupposed to be valid. And so we come to the question what nature of validity this is.”

is missing in our typescript,  where the sentence ends with

“zugrundegelegt.”

“taken as a basis.”

instead,  at the very end of page 4 of our typescript.

2.4.2 Over 16 pages entirely missing in the typescript

The remainder of  ď 1 of  [?, ?; ?]  is entirely omitted in our typescript,  i.e. everything from the penultimate paragraph on p. 3  to the very end of  p. 19  is entirely missing.  This remainder covers –  among others subjects – the following: the logical symbolism, axiomatizations of geometry, satisfiability and universal validity of formulas, the AchilleŊ Paradox, the existence of an infinite manifold, the method of arithmetization, and the task of a proof of consistency as an impossibility proof.

2.4.3 A completely unknown introduction;  from our typescript,  pp. 5–14

In ď 1 of our typescript, however, right after the very end of page 4 (just mentioned at the very end of \sectrefsection Parallel introductory part),  there is a completely unknown, most interesting, and well-written introduction to the foundations of mathematics, \hilbertplain’s proof theory, and the finitist standpoint, which seems to be entirely unpublished up to now.

We now present this introduction in the following way:  The German original is found on the pages with even page numbers and our English translation on the respectively following pages with odd page numbers.

To this end, the remainder of the current page is left blank here.

|5 Wir kommen somit zu dem zweiten der anfangŊ genannten Themata der Grundlagenuntersuchungen. In der Begrundung der AnalysiŊ ist eŊ ja im 19. Jahrhundert zuerst durch die Untersuchungen von Bolzano und Cauchy und hernach deren Weiterfuhrung und Vollendung durch Dedekind, Cantor und Weierstraȷ gelungen,333Méray, Enc. I.1, 3 (1904).  die Methoden der Infinitesimalrechnung, die ja in ihren Anfangen einer vollen Deutlichkeit entbehrten und mehr nur instinktiv gehandhabt wurden, im Sinne einer starkeren Anknupfung an die klassischen Methoden der griechischen Mathematiker Eudoxos und Archimedes zu einer prazise mitteilbaren und lehrbaren zu gestalten.

Indem diese Deutlichkeit erreicht wurde, traten zugleich die zugrundeliegenden methodischen VorauŊsetzungen mehr hervor, und man ging auch dazu *uber, diese VorauŊsetzungen uber die Zielsetzung der Infinitesimalrechnung hinauŊ syŊtematisch zu verwerten, wie eŊ ja vor allem in der Cantor’schen Mengenlehre geschah. Die hier stattfindende starke Ueberschreitung deŊ mathematisch Gewohnten weckte vielerseitŊ Kritik, die dann noch durch die Entdeckung der mengentheoretischen Paradoxien bestarkt wurde.

Wenngleich eŊ sich nun auch bei naherem Zusehen erwieŊ, daȷ eŊ zur Verhutung der Paradoxien genugte, gewisse extreme BegriffŊbildungen zu vermeiden, die tatsachlich fur den Auf bau der Mengenlehre und erst recht fur die Methoden der AnalysiŊ gar nicht erforderlich sind, so ist doch seitdem die DiŊkussion uber die Grundlagen der Mathematik nicht zur Ruhe gekommen, und man hat sich auch jener Paradoxien alŊ Argument bedient, um viel weiter gehende Einschrankungen deŊ mathematischen VerfahrenŊ zu motivieren, alŊ sie zur Behebung der Widerspr*uche |6  direkt erfordert werden.

Fur eine grundliche Stellungnahme zu dieser GrundlagendiŊkussion erscheint eine eingehende Betrachtung der logischen Struktur der mathematischen Theorien alŊ geboten.

In der Tat bemerkt man, daȷ eŊ sich bei den zur DiŊkussion stehenden Verfahren der Mathematik um Methoden deŊ FolgernŊ und der BegriffŊbildung handelt, daȷ also hier eine Art der Erweiterung der gewohnlichen Logik zur Geltung kommt. Zugleich zeigt sich eine enge Verflochtenheit deŊ Mathematischen mit dem Logischen: einerseitŊ tritt die Mengenlehre ihrem Gegenstand nach, durch die Beziehung von Mengen und Pradikaten (d. h. durch daŊ VerhaltniŊ von Umfang und Inhalt der Begriffe) in engŊte Beruhrung mit der Logik; andererseitŊ wird man in der syŊtematischen Untersuchung der logischen BildungŊformen und Schluȷweisen mit Notwendigkeit auf mathematische Betrachtungen gefuhrt. So ist ja bereitŊ die traditionelle Lehre von den kategorischen Schlussen eine typisch mathematische Untersuchung, waŊ nur durch ihre hiŊtorische Einordnung in die Philosophie leicht verdeckt wird. Mit dieser mathematischen Seite deŊ Logischen hangt eŊ auch zusammen, daȷ die logischen Schlusse – wie sie inŊbesondere bei der reichhaltigeren Anwendung der Logik in den mathematischen Theorien zur Verwendung kommen –, in einer mathematischen Weise fixierbar und auŊ einer Reihe von wenigen Elementarprozessen zusammensetzbar sind.

|5 Let us now turn to the second topic of the foundational investigations listed at the beginning, regarding the grounding of Analysis.  As is well known, in the 19 th century, first through the investigations of Bolzano and Cauchy and then through their continuation and completion by Dedekind, Cantor and Weierstraȷ,444Méray, Enc. I.1, 3 (1904). [It is difficult to say what this abbreviated footnote text by \bernaysplain’ hand means, but it probably refers to section “6. Point de vue de Ch. Méray”,   pp. 147–149 in [Pringsheim, 1904/07].  This would make sense because our typescript omits the first name to be mentioned in the list, namely Charle Méray (1835–1911),  and [Pringsheim, 1904/07] is one of the first texts that mentions the primacy of this neglected mathematician.  Note that the German original [Pringsheim, 1898] does not contain this section on Méray at all.The footnote is not executed in any of the two carbon copies (cf. \sectrefsection carbon copies) of our typescript,  but \bernaysplain probably wanted to add “Méray,” before “Dedekind” and have the expanded proper citation in a footnote.]  the methods of infinitesimal calculus, which lacked clarity and were applied more or less instinctively in their beginnings, were given a precisely communicable and teachable form, in the sense of a closer orientation toward the classical methods of the Greek mathematicians Eudoxos and Archimedes.

As this clarity was achieved, the underlying presuppositions of these methods became more obvious as well. Moreover, these presuppositions were then systematically applied beyond the field of infinitesimal calculus,  in particular in Cantor’s set theory.  The strong transgression of the common usage of these presuppositions in mathematics aroused criticism which came from many sides and was then further encouraged by the discovery of the set-theoretic paradoxes.

On a closer inspection,  however,  it turned out that the paradoxes can be averted by the exclusion of certain extreme concept formations,  which are not actually required for the constructions of set theory,  and even less for the methods of Analysis.  And yet,  the discussion on the foundations of mathematics has not settled down since then.   Moreover, those paradoxes were employed as motivational arguments for restrictions on the mathematical approach that go far beyond of what is immediately required for eliminating the contradictions.    |6

A careful positioning in this discussion on the foundations of mathematics requires a more detailed consideration of the logical structure of the mathematical theories.

Let us notice that the mathematical approaches under discussion, in fact,  consist of methods of inference and concept formation. This means that some extension of theusual logic comes to bear in these approaches.  At the same time, we notice that the mathematical and the logical are tightly intertwined here:  On the one hand, considering its objects,  set theory comes very close to logic through the relation between sets and predicates, i.e. through the relationship between extension and content of notions.  On the other hand, any systematic investigation of the modes of logical formation and inference will necessarily raise mathematical problems.  As a matter of fact, the traditional teaching of the categorical inferences is already a typical mathematical investigation;  this fact is only superficially concealed by the historical classification of this teaching into philosophy. It is also connected with this mathematical side of the logical that the logical inferences — in particular as they occur in comprehensive logic application in mathematical theories —  can be captured in a mathematical way as being composed of a small number of elementary processes.

Dieser Sachverhalt wurde zur vollen Deutlichkeit gebracht |7  durch die Entwicklung der SyŊteme der symbolischen Logik, wie sie, vorbereitet durch den Boole’schen Logikkalkul,[sic!] um die Jahrhundertwende inŊbesondere von Peirce, Frege, Schroder, Peano, Whitehead u. Russell geschaffen wurden. Bei der Konstruktion dieser SyŊteme ging man teilŊ darauf auŊ, eine handliche Symbolik zu gewinnen, die zugleich eine genauere Kontrolle der Schluȷfolgerungen ermoglichte, teilŊ bezweckte man eine Einordnung der Mathematik in die Logik.

EŊ war der Gedanke \hilbertplainŊ, die logische Symbolik dazu zu verwerten, die mathematischen BeweiŊmethoden zum Gegenstand einer mathematischen Untersuchung, einer “BeweiŊtheorie”,  zu machen.555Der erte Ansatz in dieser Richtung war der \hilbertplain’sche Heidelberger Vortrag 1904 [Hilbert, 1905], der freilich noch ganz im Fragmentarischen blieb. (In diesem wurde auch schon der Gedanke eine gemeinsamen Auf baus von Mathematik und Logik zur Geltung gebracht.)  Eine erte Weiterfuhrung dieser Gedanken findet sich, noch vor \hilbertplain spateren Untersuchungen, in dem Werk von Julius Konig: Neue Grundlagen der Logik, Arithmetik, und Mengenlehre (Leipzig, 1914) [K*onig, 1914].  Der wesentliche GesichtŊpunkt dabei ist, die Methode der formalen Axiomatik auch auf daŊ logische Schlieȷen selbst, wie eŊ in den Theorien der Arithmetik und Mengenlehre auŊgeubt wird, anzuwenden und somit an die Stelle der Prozesse der logische[n] BegriffŊbildung und Folgerung formal angesetzte Operationen treten zu lassen.  Hierdurch gewinnen wir den Vorteil,  daȷ wir bei strittigen Begriffen und Schluȷweisen nicht die inhaltliche Bedeutung in Betracht zu ziehen brauchen, sondern nur den formalen Effekt,  der durch ihre Anwendung in den deduktiven Prozessen bewirkt wird.  Dieser Effektlaȷt sich vom Standpunkt einer ganz elementaren Betrachtung verfolgen.  Wir haben sodie Moglichkeit,  Methoden,  die vom inhaltlichen Standpunkt problematisch erscheinen, alŊ beweiŊtechnische Verfahren zu akzeptieren und zu rechtfertigen.

In diesem Sinne hat \hilbertplain die Auf gabe gestellt und in Angriff genommen, daŊ SyŊtem der AnalysiŊ und Mengenlehre alŊ |8  ein widerspruchŊfreieŊ Gedankengeb*aude zu erweisen. Diese Auf gabe gliedert sich in zwei Teile.

EŊ handelt sich zunachst darum, die BeweiŊmethoden der AnalysiŊ und Mengenlehre einer formalen Axiomatik zu unterwerfen oder,  wie wir eŊ kurz nennen wollen,  zu formalisieren.  Hierfur konnte sich \hilbertplain auf die bereitŊ auŊgebildeten zuvor genanntenSyŊteme der LogiŊtik stutzen, in denen eine solche Formalisierung bereitŊ geleistet war.Der GesichtŊpunkt der streng formalen Deduktion wurde zuerst bei Frege scharf herauŊgestellt und fur Teile der Mathematik zur Durchf*uhrung gebracht.  Die Methode zur handlichen AuŊgestaltung einer Formalisierung wurde durch Peano entwickelt.  Eine Verbindung von beiden fand in den Principia Mathematica durch Whitehead und Russell statt.

Die hier[mit] vorliegende Formalisierung ist freilich fur die Zwecke der BeweiŊtheorie insofern nicht vorteilhaft,  alŊ sie keine Gliederung in elementarere und hohere Bereiche der BegriffŊbildung und deŊ SchlieȷenŊ ermoglicht.   DaŊ ruhrt davon her,  daȷ in den Principia Mathematica sowie bei Frege die Gewinnung der Zahlentheorie auŊ der allgemeinen Mengenlehre alŊ eineŊ der Haupt ziele genommen ist.  So k*onnen hier die Methoden einer elementareren Behandlung der Zahlentheorie nicht in Erscheinung treten.

This state of affairs was brought to full clarity |7  by the development of the systems of symbolic logic, which, prepared by the Boolean logic calculus, were created around the turn of the century in particular by Peirce, Frege, Schr*oder, Peano, Whitehead & Russell.  The construction of these systems partly aimed at obtaining a handy symbolism, which also facilitated a more precise control over the conclusions,  and partly aimed at a classification of mathematics into logic.

It was \hilbertplain’s idea to create a “proof theory”,   in which the mathematical proof methods, formalized in a logical symbolism, become the objects of mathematical investigation.666The first approach in this direction was \hilbertplain’s Heidelberg talk of 1904 [Hilbert, 1905], which, of course, had to remain outright fragmentary. (In this talk also the idea of a joint construction of mathematics and logic is already brought to bear.)  A first continuation of these ideas can be found, even before \hilbertplain’s later investigations, in the work of Julius K*onig:  Neue Grundlagen der Logik, Arithmetik, und Mengenlehre [New Foundations of Logic, Arithmetic, and Set Theory] (Leipzig, 1914) [K*onig, 1914].  The significant viewpoint is to apply the method of formal axiomatics also to the logical reasoning itself as it is applied in the theories of arithmetic and set theory,  and thus to let formally specified operations take the places of the processes of logical concept formation and conclusion.  This has the advantage that we need not consider the contentual meaning of contentious notions and modes of inference,  but only the formal effect of their application in deductive processes.  This effect can be traced by means of most elementary considerations.  We thus have the possibility of accepting and justifying methods as proof-technical procedures,  no matter whether they are problematic from the contentual standpoint.

In this sense,  \hilbertplain has set and tackled the task of proving the system of Analysis and set theory to be |8  a consistent construct of ideas.  This task subdivides into two parts.

First we have to represent the proof methods of Analysis and set theory in a formal axiomatics or,  as we want to call it briefly,  to formalize them.  To this end, \hilbertplain could resort to the mentioned full-fledged systems of formal mathematical logic, in which such a formalization had already been accomplished.  Frege was the first who clearly displayed the viewpoint of strict formal deduction and put it into practice for parts of mathematics.  It was Peano who first developed handy presentations for such formalizations.  In the Principia Mathematica,  Whitehead and Russell combined these accomplishments of Frege and Peano.

The formalization given by them is not advantageous for the purposes of proof theory, however, as it lacks subdividability into elementary and more advanced domains of concept formation and inference.  This lack of subdividability has its historic origin in one of the main goals of the Principia Mathematica as well as Frege’s work:  the extraction of number theory from general set theory.  Consequently,  methods for a more elementary treatment of number theory cannot appear in their formalizations.

Von einer Formalisierung fur die Zwecke der BeweiŊtheorie ist zu wunschen, daȷ sie eine analoge axiomatische Gliederung der logisch-mathematischen Bildungen und Prozesse liefert, wie sie in der *ublichen Axiomatik durch die Sonderung der Axiomengruppen bewirkt wird. Unter diesem GesichtŊpunkt erscheint ein schichtweiser Auf bau deŊ deduktiven FormaliŊmuŊ alŊ angemessen.    |9

So wurde man veranlaȷt, von neuem die Formalisierung der mathematischen DiŊziplinen vorzunehmen, und man ist dabei zur prazisen Beschreibung von naturgemaȷ abgegrenzten Teilbereichen der logisch-mathematischen Deduktion gelangt, welche sich alŊ solche zum erŊten Mal an Hand deŊ FormalisierungŊprozesseŊ darstellten.

Auf Grund der vollzogenen Formalisierung gewinnt nun die Auf gabe deŊ NachweiseŊ der WiderspruchŊfreiheit fur die arithmetischen DiŊziplinen eine bestimmtere mathematische Form. EŊ handelt sich jetzt darum, zu erkennen, daȷ die festgelegten Prozesse der AuŊsagenbildung und der Schluȷfolgerung nicht zur Herleitung solcher Satze fuhren konnen,  die einander im Sinne der gewohnlichen inhaltlichen Interpretation widersprechen.  DaŊ Widersprechen von Satzen stellt sich mittelŊ der Formalisierung der Negation durch eine einfache Beziehung der entsprechenden Satzformeln dar.

UeberdieŊ ergibt sich bei einer zweckmaȷigen Formalisierung der AuŊsagenlogik noch eine Vereinfachung in der Weise, daȷ auŊgehend von irgend einem Widerspruch jede beliebige AuŊsage deŊ formalisierten BereichŊ herleitbar wird. Auf Grund davon genugt eŊ, um die Unmoglichkeit eineŊ WiderspruchŊ in dem genannten Sinne erkennen zu lassen, daȷ man daŊ Gegenteil eineŊ bestimmten einzelnen elementar gultigen SatzeŊ alŊ nicht herleitbar erweist. Die AuŊfuhrung eineŊ solchen NachweiseŊ – anschlieȷend an den schrittweisen Auf stieg der Teilbereiche – bildet den zweiten Teil deŊ \hilbertplain’schen ProgrammŊ. Die Durchfuhrung ist freilich \hilbertplain nicht gelungen, und eŊ ist auch heute noch nicht abzusehen, ob – oder vielmehr in welchem Sinne – sie gelingen kann.    |10

EŊ bestehen namlich hier nicht nur groȷe technische,  sondern auch grundsatzliche Schwierigkeiten. Diese erheben sich vor allem mit Bezug auf die Frage,  welche Mittel fur den gewunschten NachweiŊ zugelassen werden sollen.  In der Tat ging ja daŊ BedurfniŊ fur einen solchen NachweiŊ von einer Kritik der *ublichen BeweiŊmethoden auŊ.  Soll dieser Kritik Rechnung getragen werden,  so darf der NachweiŊ der WiderspruchŊfreiheit nicht seinerseitŊ auf einer Verwendung der kritisierten Methoden beruhen.

Durch diese Erwagung erhalten wir aber zunachst nur eine Abgrenzung im negativen Sinne,  und eŊ bleibt noch die Auf gabe,  genauer zu bestimmen,  auf welche Arten der Ueberlegung die BeweiŊtheorie sich stutzen soll.  Fur die Wahl dieseŊ StandpunktŊ wird unŊ ein Anhalt durch daŊ ErforderniŊ gegeben,  daȷ zumindest ja die Behauptung der WiderspruchŊfreiheit fur die formalisierten Theorien sich prazise fassen lassen muȷ.

It is to be desired from a formalization for the purposes of proof theory that it admits an axiomatic subdivision of the logico-mathematical formations and processes that is analogous to the effect of the separation of axioms into different groups,  as it is often found in customary axiomatics.  From this viewpoint,  it appears to be adequate to construct the deductive formalism in layers.    |9

Therefore,  the formalization of the mathematical disciplines was put on the agenda again.  And,  in the course of the resulting formalization process,  naturally separated sub-domains of logico-mathematical deduction were brought into separate being for the first time,together with their precise descriptions.

On the basis of the given formalization,  the task of proving the consistency of the arithmetical disciplines now gains a more definite mathematical form.  It now means to realize that the uniquely defined processes of conclusion and of proposition formation cannot lead to the derivation of sentences that contradict each other according to the common contentual interpretation.  By means of the formalization of negation,  a contradiction of sentences canbe represented simply as the occurrence of two corresponding formalized sentences.777[This sentence may mean two different things;  in the order of preference:   1.  “The realization of sentences that contradict each other can be reduced to tracing the derivation of two sentences of the forms $A$ and $\overline{A}$.”   Soundness of this problem reduction requires that the derivation process satisfies ex falso quodlibet,  and completeness of the reduction requires a certain form of completeness of the derivation process. The latter, for instance, is not given for the derivation process in [Wirth & Stolzenburg, 2016,  2.2].2.  “Contradiction may be defined in this context as two derivable sentences of the forms $A$ and $\overline{A}$.”]

Moreover,  there is a further simplification by the fact that,  for a formalization of propositional logic appropriate for our purposes,  an arbitrary contradiction will admit the derivation of each and every proposition of the formalized domain.  To realize the impossibility of a contradiction in the mentioned sense,  it thus suffices to pick any definite, elementary valid sentence and show that the opposite of this sentence cannot be derived. After the stepwise construction of the subdomains,  it is the execution of such a proof which forms the second part of \hilbertplain’Ŋ program.  Admittedly,  this execution was not achieved by \hilbertplain,  and even today it is still not foreseeable whether — or rather in which sense — it may be achieved.    |10

In fact, there are not only major technical difficulties here, but also fundamental ones.  These arise mainly with regard to the question, which means are to be admitted for the desired proof.   It was,  after all,  a critique of the customary proof methods that prompted the demand for such a proof.   If this critique is to be taken into proper account,  then the proof of consistency must not in turn rely on the application of the criticized methods.

By this consideration, however, we get only a first boundary in the negative sense;  and the task still remains to determine more precisely,  on which sorts of consideration proof theory is to be based.  A hint on the choice of this standpoint is given by the requirementthat at least the assertion of consistency must be precisely expressible for the formalized theories.

Diesem ErforderniŊ wird bereitŊ genugt durch eine Art der elementaren mathemati-schen BetrachtungŊweise,  welche \hilbertplain alŊ den finiten Standpunkt  bezeichnet hat.EŊ ist diejenige Art anschaulicher mathematischer Ueberlegung,  wie sie in der elementa-ren Kombinatorik angewandt wird.  Auch die elementare Zahlentheorie und Buchstaben-Algebra laȷt sich auf diese Art behandeln.   DaŊ Kennzeichende f*ur die finite Betrachtung besteht in folgenden Momenten:

AlŊ Gegenst*ande werden nur endliche Gebilde genommen, an denen auch nur diskrete GestaltŊmerkmale unterschieden werden. 2. 2.

Die Formen deŊ allgemeinen und deŊ exiŊtentialen UrteilŊ kommen nur auf eine eingeschrankte Art zur Anwendung, im Sinne |11  der Vermeidung der Vorstellung von unendlichen Gesamtheiten; namlich daŊ allgemeine Urteil wird nur in hypothetischem Sinne gebraucht, alŊ eine AuŊsage uber jedweden vorliegenden Einzelfall, und daŊ exiŊtentiale Urteil alŊ ein (zweckmaȷig zu vermerkender) Teil einer naher bestimmten Feststellung, in der entweder ein bestimmt strukturierteŊ Gebilde vorgewiesen oder ein allgemeineŊ Verfahren auf gezeigt wird, nach dem man zu einem (gewisse Bedingungen erfullenden) Gegenstand888[This must be the plural in general: “Gegenst*anden”.] einen anderen Gegenstand mit verlangten Eigenschaften gewinnen kann. 3. 3.

Alle Annahmen, die man einf*uhrt, beziehen sich auf endliche Konfigurationen.

Mit der genaueren Beschreibung und Erorterung der finiten BetrachtungŊweise werden wir unŊ noch deŊ Naheren zu befassen haben.

EŊ ware zweifel loŊ sehr befriedigend, wenn wir unŊ in der beweiŊtheoretischen Untersuchung vollig an diesen Rahmen elementarer Betrachtung halten konnten. Die Moglichkeit hierfur scheint zunachst insofern gegeben zu sein, alŊ ja mit Bezug auf eine formalisierte Theorie die Behauptung ihrer WiderspruchŊfreiheit sich nach dem vorhin Bemerkten in finiter Form dahin auŊsprechen laȷt, daȷ ein jeder formalisierte BeweiŊ eine Endformel hat, die verschieden ist von der Negation einer bestimmten[,] geeignet gewahlten Satzformel.

This requirement is already satisfied by a form of elementary mathematical mode of consideration, which \hilbertplain called the finitist standpoint.   It is the form of those intuitivemathematical considerations which are applied in elementary combinatorics.  Also elementary number theory and algebra can be treated in this form.   The characteristics of finitist considerations are given by the following moments:

The objects must be finite entities,  distinguished only by their discrete  attributes. 2. 2.

Universal and existential judgments may occur only if  |11  they do not refer to the conception of any infinite totality:  The universal judgment may be used only in the hypothetical sense,  as a proposition on any individual object to be given.  Moreover,  the existential judgment may occur only as  (an appropriately noted)  part of a more specifically determined statement,  which additionally presents either an entityof definite structure,  or else a general procedure for generating an object of theasserted properties from any object[s] to be given (satisfying certain conditions).999[The objects which the general procedure (to be presented here)  must accept as input arguments are those individual objects which may be given to the universal judgments on which the existential judgment depends,  i.e. in whose scope the existential judgment occurs.   See [?, ?; ?]  for several formal frameworks where this statement makes sense even in the absence of quantifiers.The conditions that these individual objects may be assumed to satisfy (according to “gewisse Bedingungen erf*ullenden”/“satisfying certain conditions”)  are those which arise from the logical context of the existential judgment, e.g. for an existential judgment in the conclusion of an implication the individual objects may be assumed to satisfy the condition of the implication \etc   The required form of reasoning with this kind of logical context,  called hierarchical contextual reasoning,  was nicely formalized in [Autexier, 2003]  for the first time.] 3. 3.

Assumptions may be introduced only if they refer to finite configurations.

We will have to take a closer look on a more detailed description and discussion of the finitist mode of consideration later.

There can be no doubt that it would be very fulfilling if we were able to confine our proof-theoretic investigations to this framework of elementary consideration.  At first, this seems to be possible insofar as  — according to what we have previously noticed —the assertion of the consistency of a formalized theory can be expressed in finitist form by the assertion that every formalized proof has an end formula that is different from the negation of a definite, properly chosen formalized sentence.

Die Formulierbarkeit eineŊ ProblemŊ im Rahmen gewisser AuŊdruckŊmittel bietet aber noch keine Gewahr dafur, daȷ seine Losung sich mit diesen Mitteln bewerkstelligen laȷt. Tatsachlich hat eŊ sich im Fall der BeweiŊtheorie herauŊgestellt, daȷ fur die gewunschten Nachweise der WiderspruchŊfreiheit formalisierter Theorien die finiten Methoden nicht zulanglich sind.  |12  Man hat sich so genotigt gesehen, fur die BeweiŊtheorie den ursprunglichen finiten Standpunkt zu einem “konstruktiven” Standpunkt zu erweitern, der sich etwa so kennzeichen laȷt, daȷ von den drei soeben genannten Forderungen nur die erŊten beiden auf rechterhalten werden, die dritte aber fallen gelassen wird. So kommt man dazu, fur die BeweiŊtheorie eine ungefahr solche methodische Haltung einzunehmen, wie sie der Brouwer’sche IntuitioniŊmuŊ fur die Mathematik uberhaupt alŊ einzig zulassig ansieht.101010Eine prazise Vergleichung ist darum hier nicht zu verlangen, weil die intuitionistische Haltung nicht durch Gebrauchregeln, sondern durch eine philosophische Einstellung charakterisiert ist.  Das wird auch von Heyting ungeachtet der von ihm durchgefuhrten Formalisierung der intuitionistischen Logik und Mathematik hervorgehoben.  Fur eine Konfrontierung der Methoden der konstruktiven Beweitheorie mit denen de Intuitionimu sind auch die neueren Untersuchungen von G. F. C. Griss  uber die negationfreie intuitionistische Mathematik von Belang, bei welchen da Operieren mit irrealen (unerfullten) Annahmen grunds*atzlich vermieden wird (Proc. Kon. Ned. Adad. v. Wetensch. 49 (1946) [Griss, 1946],   53 (1950) [Griss, 1950]  und  54 (1951) [?, ?; ?; ?; ?][)].

Doch selbst bei dieser Erweiterung deŊ finiten StandpunktŊ hat eŊ nicht allenthalben sein Bewenden. Man sieht sich vielmehr bei der Behandlung gewisser Fragen dazu gedrangt, auch die zweite der obigen Forderungen fallen zu lassen. DieŊ ist zum Beispiel bei der Behandlung der Frage der Vollstandigkeit deŊ SyŊtemŊ der Regeln fur die gewohnliche Pradikatenlogik der Fall, die zuerst von Kurt  Godel im positiven Sinne gelost worden ist. Hier erfordert bereitŊ die Formulierung deŊ ErgebnisseŊ, wenigŊtenŊ wenn man sie in pragnanter und einfacher Form haben will, die Einfuhrung einer nichtkonstruktiven BegriffŊbildung. Eine finite Fassung deŊ ErgebnisseŊ und auch ein BeweiŊ im finiten Rahmen laȷt sich erzwingen, ist aber mit technischen Komplikationen belastet.

DieseŊ Beispiel deŊ Godel’schen VollstandigkeitŊsatzeŊ ist zugleich dafur charakteriŊtisch, daȷ die beweiŊtheoretische Fragestellung in ihrer naturlichen AuŊgestaltung nicht bei dem Problem verbleibt, welcheŊ auŊ der Kritik der *ublichen Verfahren der klassischen Mathematik erwachsen ist.  Auch \hilbertplain hat ja von vornherein die Auf gabe der BeweiŊtheorie sehr weit gefaȷt.111111Vgl. seine Aeuæerungen in dem Vortrag: Axiomatisches Denken (Math. Ann. 78, pp. 405–415 (1918)) [Hilbert, 1918].    |13

Unter den weitergehenden Fragestellungen sind nun auch etliche solche, bei denen die Verbindlichkeit der Anforderung einer methodischen Beschrankung alŊ fraglich erscheint. So sind in neuerer Zeit verschiedenen erfolgreiche Untersuchungen, die in weiterem Sinne zum Felde der BeweiŊtheorie gehoren, im Rahmen der ublichen mathematischen Methodik, also ohne Beschrankung der BegriffŊbildungen und BeweiŊmethoden, durchgefuhrt worden. AndererseitŊ haben verschiedene Autoren fur jene speziellen beweiŊtheoretischen Untersuchungen, die eŊ mit den Fragen der WiderspruchŊfreiheit zu tun haben, einen solchen Standpunkt gew*ahlt, bei welchem von den drei vorhin formulierten Forderungen nur die erŊte zugrunde gelegt wird.

The expressibility of a problem within the limits of certain means of expression,  however,  does not guarantee that its solution can be accomplished with these means as well.  For the case of proof theory,  it has indeed turned out that the finitist methods are not sufficient for the desired proofs of consistency of formalized theories.121212[Can this refer to anything else but [G*odel, 1931] ?]  |12  Therefore,  it became necessary to extend the original finitist standpoint for proof theory to a “constructive” one,  which can be characterized roughly by maintaining only the first two requirements of the three just mentioned ones,  but dropping the third.  Thus,  we arrive at at position toward the methods in proof theory which is roughly the one that Brouwer’s intuitionism considers to be the only admissible one in mathematics in general.131313A precise comparison is not to be demanded here,  because the intuitionist position is actually not characterized by rules of application,  but by a philosophical attitude.  This is emphasized also by Heyting,  notwithstanding his formalization of intuitionist logic and mathematics.  Moreover,  a most relevant comparison of the methods of constructive proof theory with those of intuitionism is found in the more recent investigations of  G. F. C. Griss   on negation-free intuitionist mathematics,  where the handling of unreal (i.e. unsatisfiable) assumptions is avoided on principle (Proc. Kon. Ned. Adad. v. Wetensch. 49 (1946) [Griss, 1946],   53 (1950) [Griss, 1950]  and  54 (1951) [?, ?; ?; ?; ?]).

Even this extension of the finitist standpoint,  however,  does not suffice in all cases.  In fact,  for treating certain problems,  we feel urged to drop the second of the above requirements as well.  This is for example the case for the treatment of the problem of completeness of the rule system for ordinary predicate logic,  first solved by Kurt  Godel — in the positive sense.   In this example,  a concise and simple expression of the result already requires the introduction of a non-constructive concept formation.  A finitist version of the result can be enforced,  and also a proof by finitist means,  but these versions are burdened with technical complication.141414[This seems to be a reference to Herbrand’ Fundamental Theorem [Herbrand, 1930], which, together with the Lowenheim–Skolem Theorem [Löwenheim, 1915], yields a finitist version of G*odel’s completeness theorem [G*odel, 1930], cf. e.g. [?, ?; ?], [?, ?; ?].]

Thus,  G*odel’s completeness theorem provides also a characteristic example that proof-theoretic problem definitions in their natural embodiment already exceed the problem that resulted from the critique of the customary procedures in classical mathematics.  Accordingly,  \hilbertplain already gave a comprehensive outlook on the tasks of proof theory from the very beginning.151515Cf. his statements in his talk: Axiomatisches Denken [Axiomatic Tought] (Math. Ann. 78, pp. 405–415 (1918)) [Hilbert, 1918].    |13

Moreover,  for quite a few among the more advanced problem definitions,  the commitment to a restriction of the methods may be questioned anyway.  In fact,  in more recent times,  in the field of proof theory in the broader sense,  various successful investigations have been realized with the full methodology of customary mathematics,  restricting neither concept formations nor proof methods.  Furthermore,  for proof-theoretic investigations explicitly concerned with the problems of consistency,  however,  various authors have chosen a standpoint that relies only on the first of the three previously stated restrictions.

Eine endgultige Entscheidung der Methodenfrage kann dieser Sachlage gegenuber jedenfallŊ nur erwartet werden, wenn man einen Ueberblick daruber hat, waŊ die verschiedenen Methoden zu leisten vermogen. EŊ kann schwerlich behauptet werden, daȷ gegenwartig eine Entscheidung jener Frage vorliegt, die nicht bloȷ durch eine vorgefaȷte philosophische Ansicht bestimmt ist. Und bezuglich der verschiedenen sich bekampfenden und heute ublichermaȷen gegenubergestellten philosophischen Lehrmeinungen besteht der Verdacht, daȷ sie ungeklarte VorauŊsetzungen in sich schlieȷen, die ihrerseitŊ vielleicht eher fragw*urdig sind alŊ die angefochtenen mathematischen Theorien.

AngesichtŊ dieser Sachlage erscheint eŊ alŊ daŊ angemessene Verfahren, daȷ wir einerseitŊ die methodische Richtlinie, die durch den GesichtŊpunkt der finiten Betrachtung gegeben wird, im Auge behalten, andererseitŊ unŊ [aber dadurch] nicht in der Methode festlegen.  Dabei ist inŊbesondere der Umstand mitbestimmend, daȷ neuerdingŊ die beweiŊtheoretischen Untersuchungen in einen engeren Kontakt getreten sind mit den allgemeinen Theorien der abŊtrakten Algebra und Topologie,  |14  so daȷ die AuŊsicht sich er*offnet, daȷ die beweiŊtheoretischen Methoden zu einem wirkungŊvollen HilfŊmittel in diesen Gebieten sich entwickeln.   Bei solchen Anwendungen fungiert die BeweiŊtheorie nicht in der Rolle der BeweiŊkritik, sondern im Rahmen der ublichen Methoden deŊ mathematischen SchlieȷenŊ, und eŊ wurde darum hier die Forderung der finiten BetrachtungŊweise gar nicht am Platze sein.

—

Zur Vorbereitung unserer beweiŊtheoretischen Betrachtungen ist eŊ nun auf jeden Fall w*unschenŊwert, daȷ die spezifische Art der finiten Ueberlegung deutlich gemacht werde. Zur Illustrierung eignet sich besonderŊ daŊ Gebiet der elementaren Zahlentheorie, in welcher der Standpunkt der direkten inhaltlichen, ohne axiomatische Annahmen sich vollziehenden Ueberlegungen am reinsten auŊgebildet ist.    |15

In any case — confronted with this overall situation —  a final answer to the question which methods to choose can only be expected after attaining a comprehensive insight into the full capability of the different methods.  It can hardly be claimed that an answer to that question has been given until today,  unless determined by preconceived philosophical beliefs.  And the various competing philosophical doctrines  —  nowadays mostly confronted with each other161616[The English phrase “confronted with each other” is just as ambiguous as the German original “gegen*ubergestellt”,   meaning either to be brought into opposition or to be arranged face-to-face for a comparison.] —  are suspected to comprise uncleared presuppositions.   Moreover,  these presuppositions may well be more questionable in turn than the mathematical theories under challenge.

In view of this situation,  the appropriate procedure seems to be that we will keep track of the viewpoint of a finitist treatment as a guideline to determine our method of choice,  but do not strictly limit ourselves to this method.   A particular reason for this non-limitation is the fact that recently the proof-theoretic investigations have come into closer contact with the general theories of abstract algebra and topology,171717[To what can this refer?  Is there any candidate prior to [Hasenjaeger, 1950c], entitled “Topologische Untersuchungen zur Semantik und Syntax eine erweiterten Pradikatenkalkul” (“Topological Investigations on Semantics and Syntax of an Extended Predicate Calculus”) ?]   |14  and thus the prospect is opening up that the proof-theoretic methods may develop into a powerful tool in these fields.   In such applications,  proof theory does not act in the rôle of a proof critique,  but within the framework of the customary methods of mathematical inference,  and therefore the demand for a finitist mode of consideration would not be appropriate here at all.

—

For the preparation of our proof-theoretic considerations,  it is now desirable in any case that the specific mode of finitist considerations is demonstrated.  Particularly suitable for such an illustration is the field of elementary number theory,  where the standpoint of direct contentual consideration without axiomatic assumptions is developed most purely.    |15

With the previous paragraph ends our long excerpt from our typescript and its ď 1, presented here together with its English translation on the right-hand side pages (i.e. those with uneven numbers).

2.5 Discussion and Excerpts of  ď 2 of  Our Typescript

ď 2 of our typescript comes with the subsection headline “ď 2. Die elementare Zahlentheorie” (“ď 2. Elementary Number Theory”)  and contains a version similar to the first nine pages (pp. 20–28)  of  ď 2 of  [?, ?; ?],  which comes with a similar headline:

“ď 2.  Die elementare Zahlentheorie.  —  DaŊ finite Schlieȷen und seine Grenzen.”

In English:

“ď 2.  Elementary Number Theory.  —   Finitist Inference and its Limits.”

The first five paragraphs of  ď 2 of  [?, ?; ?],  however,  are missing in our typescript.   For the first of these paragraphs, this is just a consequence of the omission of several paragraphs at the beginning of  ď 1 (cf. our \sectrefsection Parallel introductory part),  because it is again on the subject of the “existential form”.    The further four of these paragraphs missing in our typescript contain a digression into the subject of geometry.

2.5.1 A sentence following the second edition instead of the first one

A significant difference to [Hilbert & Bernays, 1934] is that  — instead of the paragraph

“Diese Figuren bilden eine Art von Ziffern; wir wollen hier daŊ Wort ’Ziffer‘  schlechtweg zur Bezeichnung dieser Figuren gebrauchen.”

“These figures constitute a kind of numeral; and we will simply use the word ‘numeral’  to designate just these figures.”

of [Hilbert & Bernays, 1934, p. 21]”  —  we find in our typescript the following sentence of [Hilbert & Bernays, 1968, p. 21]:

“Wir wollen diese Figuren, mit einer leichten Abweichung vom gewohnten Sprachgebrauch,  alŊ ’Ziffern‘  bezeichen.”

“Deviating slightly from the common usage of language, we will call these figures ‘numerals’.”

It is unlikely that this text was just copied from the second edition, however, because our typescript contains the addition “(in Ermangelung eineŊ besseren kurzen AuŊdruckŊ)” (“(lacking a better short expression)”),  which is deleted by \bernaysplain’ hand.

2.5.2 A significant improvement compared to both editions

Another significant difference in our typescript occurs in the enumerated list of five elements found on page 21f. in both editions of Vol. I [?, ?; ?].  This list describes the syntactic form of the “Zeichen zur Mit teilung” (“symbols for communication”):  In item 1 we read

“kleine deutsche Buchstaben zur Bezeichnung f*ur unbestimmt gelassene Ziffern;”

“small German letters for designating numerals that are left undetermined;”

in our typescript,  instead of

“Kleine deutsche Buchstaben zur Bezeichnung f*ur irgendeine nicht festgelegte Ziffer;”

“Small German letters for designating an arbitrary, not determined numeral;”

found in both editions of “\grundlagendermathematiknoindex”.

Together with other hints on the finitist standpoint found in our typescript, this correction was crucial for a change in translation in the third English edition [Hilbert & Bernays, 2017a],  as compared to the first two English editions where we translated the latter German term — after communication with several members of the advisory board of the \hilbertplain–\bernaysplain Project, who agreed that the meaning is ambiguous — with the similarly ambiguous term “an arbitrary indeterminate numeral”.181818As long as we were not able to give the German term a unique reading, we had to be careful and use a translation that does not cut off any possibly meaningful reading.  It was our typescript here that provided the information for such a unique reading.  Now we can translate that reading and do not have to bother our readers with an ambiguous English term.  As long as there are several possible readings, a translator must not give only his favorite interpretation of the original in the translation.  If the translator knows exactly what is meant, however, then that meaning should to be captured in the translation as clearly and unambiguously as possible;  otherwise the translator would propagate the weed of imperfect expression that always comes with the crop, in particular regarding the fruits of science.   Our new translation in the third edition is

“small German letters for designating arbitrary, not determined numerals;”

This new version clearly disambiguates these small German letters from formal191919Whereas German letters — all over [?, ?; ?; ?; ?] — do not denote formal variables (as Latin letters do),  in the metalogical, finitist framework, depending on the natural-language context, German letters may be used both for free atoms and for free variables in the terminology of [Wirth, 2017] (both of which are substantially different from the (bound and free) individual variables and the free formula variables of \hilbertplain–\bernaysplain).The technical term “atom” is from set theories (with atoms or urelements) and comes implicitly with a universal quantification (such as in the equations on p. 30 of [?, ?; ?; ?]),  whereas the term “free variable” is from free-variable semantic tableaus [?, ?; ?]  and comes implicitly with an ($\varepsilon$-restricted) existential quantification (such as in the equations on p. 28 of [?, ?; ?; ?]). variables as well as from arbitrary objects in the sense of ? [Fine, 1985].

For a more detailed discussion see Note 21.6 on p. 21.b in the third English edition [Hilbert & Bernays, 2017a].

2.6 Discussion and Excerpts of  ď 3 of  Our Typescript

ď 3 is the final section of our typescript.   It comes with the subsection headline  “ď 3. Ueberschreitung deŊ finiten StandpunkteŊ im mathematischen Schlieȷen.”  (“ď 3. Transgression of the finitist standpoint in mathematical inference.”).

2.6.1 From our typescript: the entire text of  ď 3,

 pp. 32–34

In its first two paragraphs of  ď 3,  our typescript announces to discuss the most interesting and critical approach to finitism chosen in the penultimate paragraph of  ď 1 of our typescript.  In the penultimate paragraphs on Pages 2.4.3 and 2.4.3 here,  we have quoted the sentence on this choice and translated it as follows:

“In view of this situation,  the appropriate procedure seems to be that we will keep track of the viewpoint of a finitist treatment as a guideline to determine our method of choice,  but do not strictly limit ourselves to this method.”

The bad news is that ď 3 is obviously truncated in our typescript: It breaks off abruptly after the first discussion of an abstract example on mathematical induction, not covering all what was announced in its first two paragraphs.

As this truncation results in a very short, but most interesting section (pp. 32–34),  we present this section here in total,  in the same way we presented the new introduction from ď 1 in \sectrefsection A completely new introduction:   The German original is found on the pages with even page numbers and our English translation on the respectively following pages with odd page numbers.

To this end, the remainder of the current page is left blank here.

Unsere auŊgefuhrte Betrachtung der AnfangŊgrunde der Zahlentheorie diente dazu, unŊ daŊ direkte inhaltliche, in Gedankenexperimenten an anschaulich vorgestellten Objekten sich vollziehende und von axiomatischen Annahmen freie Schlieȷen in seiner Anwendung und Handhabung vorzufuhren. Wir haben unŊ dabei an die methodische Einstellung gehalten, die wir anfangŊ nach \hilbertplain alŊ den “finiten Standpunkt” bezeichnet haben. Wir wollen nun deŊ naheren betrachten, wie man dazu veranlaȷt wird, den finiten Standpunkt zu uberschreiten. Dabei wollen wir anknupfen an die fruher gegebene Kennzeichnung deŊ finiten StandpunkteŊ, die ja mittelŊ der drei charakteriŊtischen Momente erfolgte:   1. Beschrankung der Gegenstande auf endliche diŊkrete Gebilde;   2. Beschrankung der Anwendung der logischen Formen deŊ allgemeinen und deŊ exiŊtentialen UrteilŊ im Sinne der Vermeidung der Vorstellung von fertigen unendlichen Gesamtheiten;   3. Beschr*ankung der Annahmen auf solche *uber endliche Konfigurationen.

Diese Momente sind geordnet im Sinne einer zunehmenden Anforderung. Wir werden nun bei der Betrachtung der Ueberschreitung deŊ finiten StandpunkteŊ naturgem*aȷ in entgegengesetzter Reihenfolge, im Sinne einer schrittweisen Abstreifung der Anforderungen, verfahren.    |33

Ein Verstoȷ gegen die dritte Forderung, wonach alle Annahmen sich auf endliche Konfigurationen beziehen sollen, liegt bereitŊ uberall da vor, wo man die Annahme der Gultigkeit eineŊ allgemeinen SatzeŊ uber Ziffern einfuhrt.

Eine Veranlassung dazu ist inŊbesondere gegeben bei Anwendung der vollstandigen Induktion zum Beweise von Satzen, welche eine Beziehung  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  fur beliebige Ziffern  m,  n  behaupten.  Soll die Induktion, etwa nach  n,  im finiten Sinne erfolgen, so muȷ bei dem Schluȷ von  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  auf  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  die Ziffer m  festgehalten werden. In dieser Weise sind wir auch im vorigen Paragraphen bei den Beweisen der Rechengesetze fur Summe und Produkt verfahren.

Haufig wird aber die vollstandige Induktion so angewandt, daȷ man zunachst zeigt, daȷ fur jede Ziffer m  die Beziehung  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},1)}}$  besteht, und sodann beweist, daȷ, fallŊ fur die Ziffer n  bei jeder beliebigen Ziffer m   $\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}$  besteht, dann auch bei jeder Ziffer m   $\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}$  besteht. Man schlieȷt darauŊ nach der vollstandigen Induktion, daȷ fur jede Ziffer n  gilt, daȷ fur jede Ziffer m   $\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}$  besteht.

Hier hat man in der zweiten zu beweisenden Behauptung einen Allsatz alŊ Pramisse;  eŊ wird ja angenommen, daȷ (fur den fixierten Wert n)  bei jeder Ziffer m  die Beziehung  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  bestehe. DieseŊ VorauŊgesetzte konnen wir unŊ nicht in der Vorstellung eigentlich vergegenwartigen.

Our treatment of the basics of number theory was meant to demonstrate the application and the use of direct contentual inference in thought experiments on intuitively conceived objects,  free of axiomatic assumptions.202020[This sentence is very similar to the first sentence of the third paragraph on p. 32 in [?, ?; ?; ?].]  In this treatment,  we have observed the methodological attitude we initially called the “finitist standpoint” according to \hilbertplain.  We now want to discuss in more detail what may be the cause for a transgression of the finitist standpoint.  We want to follow here the previously given characterization of the finitist standpoint by means of three characteristic moments:   1. limitation of any object to be a finite discrete entity;   2. limitation of any application of the logical forms of the universal and the existential judgment to avoid the conception of any infinite completed totality;   3. limitation of any assumption to refer only to finite configurations.

These moments are ordered by increasing demand.  Now,  in our discussion of the transgression of the finitist standpoint — in the sense of a stepwise discarding of demands — we will naturally proceed in the reverse order.    |33

A violation of the third requirement,  according to which all assumptions should refer to finite configurations,  is already given wherever one introduces the assumption of the validity of a universal sentence about numerals.

In particular,  a cause for such a violation may be given in an application of mathematical induction for the proof of a sentence that asserts a relation  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  for arbitrary numerals  m,  n.   If the induction,  say on  n,  is to be carried out in the finitist sense,  then the numeral m  must be held constant in the conclusion step from  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  to  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$.   In this way we proceeded also in the previous section in the proofs of the laws of calculation for sum and product.

Frequently,  however,  mathematical induction is applied in such a way that one first shows that the relation  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},1)}}$  holds for every numeral m,  and then proves for the numeral n  that  $\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}$  holds for every numeral m,  under the assumption that  $\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}$  holds for any numeral m.   From this,  we may conclude by mathematical induction for every numeral n :   $\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}$  holds for every numeral m.

In the second assertion to be shown here,  we have a universal sentence as premise;  indeed,we assume that (for the fixed value n)  the relation  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  holds for every numeral m.   In our conception,  we are not really able to bring clearly to our mind what we have to presuppose here.212121[Indeed,  we cannot visualize — element by element — the set  ${\{\ }{\mathchoice{{\mbox{\scriptscriptfrak A}}}{{\mbox{\scriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\scriptscriptfrak z}}}{{\mbox{\scriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}},\mathchoice{{\mbox{\scriptscriptfrak n}}}{{\mbox{\scriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$ $|$  $\mathchoice{{\mbox{\scriptscriptfrak z}}}{{\mbox{\scriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}{\,\in\,}{{\bf N}}{\ \}}$  of all potential assumptions,  but only effectively given, finite subsets of it.]

Freilich laȷt sich in vielen Fallen die genannte Form der Anwendung der vollstandigen Induktion vom finiten Standpunkt motivieren.  DaŊ ist z. B. dann der Fall, wenn beim BeweiŊ deŊ BestehenŊ von  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  fur ein bestimmteŊ m  die VorauŊsetzung deŊ BestehenŊ von  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath z}}}{{\mbox{\fraknomath z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  f*ur beliebige z  nur  |34  in solcher Weise zur Anwendung kommt, daȷ eine durch m und n bestimmte endliche Anzahl von Beziehungen

(1) ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{1},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}{,\ \ }\ldots{,\ \ }{\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{\mathchoice{{\mbox{\fraknomath r}}}{{\mbox{\fraknomath r}}}{{\mbox{\scriptscriptscriptfrak r}}}{{\mbox{\scriptscriptscriptfrak r}}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$    

benutzt wird, worin $\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{1},\ldots,\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{\mathchoice{{\mbox{\fraknomath r}}}{{\mbox{\fraknomath r}}}{{\mbox{\scriptscriptscriptfrak r}}}{{\mbox{\scriptscriptscriptfrak r}}}}$ gewisse auŊ m und n zu ermittelnde Ziffern sind.

In diesem Falle kommt ja der BeweiŊ deŊ hypothetischen SatzeŊ mit der Allpramisse darauf hinauŊ, daȷ man zeigt, daȷ sich die Feststellung der Beziehung  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  (fur die fixierten Ziffern m, n)  zuruckfuhren l*aȷt auf die Feststellung der Beziehungen (1), und damit ist ein Regreȷ gegeben, der die Feststellung von  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  in einer begrenzten Zahl von Schritten auf die Feststellung von Beziehungen

${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath z}}}{{\mbox{\fraknomath z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}_{1},1)}}{,\ \ }\ldots{,\ \ }{\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath z}}}{{\mbox{\fraknomath z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}_{\,\mathchoice{{\mbox{\fraknomath\char 141\relax}}}{{\mbox{\fraknomath\char 141\relax}}}{{\mbox{\scriptscriptscriptfrak\char 141\relax}}}{{\mbox{\scriptscriptscriptfrak\char 141\relax}}}},1)}}$

zuruckfuhrt, und fur diese wird durch den anfanglichen BeweiŊ deŊ BestehenŊ von  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},1)}}$  f*ur beliebige m  daŊ allgemeine Verfahren gegeben.

Diese Art der Rechtfertigung der erweiterten Form der vollstandigen Induktion mit Allsatzen alŊ Pramissen ist jedoch nicht generell anwendbar. InŊbesondere erwachst eine Schwierigkeit auŊ dem Umstand, daȷ derartige erweiterte Induktionen in komplizierter Weise ineinandergeschachtelt sein konnen. Wir wollen einen typischen Fall dieser Art naher betrachten. EŊ handelt sich dabei um einen konstruktiv behandelbaren Teil der Cantorschen Theorie der tranŊfiniten Ordinalzahlen.    |35

In many cases it is in fact possible to justify the considered application of mathematical induction from the finitist standpoint.222222[For a formal treatment of this motivation see pp. 348–351 of [?, ?; ?].]  For instance, such a justification is always possible if— in the proof  that  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  holds for a particular m   —   the application the hypothesis that   ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath z}}}{{\mbox{\fraknomath z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$  holds for arbitrary z  can be restricted  |34  to a finite number of  [instances of this universal sentence in the form of ]  relations 

(1) ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{1},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}{,\ \ }\ldots{,\ \ }{\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{\mathchoice{{\mbox{\fraknomath r}}}{{\mbox{\fraknomath r}}}{{\mbox{\scriptscriptscriptfrak r}}}{{\mbox{\scriptscriptscriptfrak r}}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}})}}$,    

where  r  as well as  $\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{1},\ldots,\mathchoice{{\mbox{\fraknomath k}}}{{\mbox{\fraknomath k}}}{{\mbox{\scriptscriptscriptfrak k}}}{{\mbox{\scriptscriptscriptfrak k}}}_{\mathchoice{{\mbox{\fraknomath r}}}{{\mbox{\fraknomath r}}}{{\mbox{\scriptscriptscriptfrak r}}}{{\mbox{\scriptscriptscriptfrak r}}}}$  are certain numerals that must be determined from m and n.

In this case the proof of the proposition232323[The occurrence of  “hypothetischen” in the German original is to make clear that “Satzes” (“sentence”) does not refer to a theorem, but just to a proposition, namely the induction step here.  The German wording clashes with the standard notion of an induction hypothesis.  Indeed,  we cannot translate this occurrence as “hypothetical sentence” here because we already translated “Vorausetzung” (“presupposition”) in the previous paragraph as “hypothesis”.] with the universal premise amounts to showing that the verification of the relation  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  (for the fixed numerals m, n)  can be reduced to the verification of the relations (1).   And therefore,  we are then given a regression procedure that reduces the verification of  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},\mathchoice{{\mbox{\fraknomath n}}}{{\mbox{\fraknomath n}}}{{\mbox{\scriptscriptscriptfrak n}}}{{\mbox{\scriptscriptscriptfrak n}}}\hskip 0.39993pt{+}1)}}$  to the verification of relations

${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath z}}}{{\mbox{\fraknomath z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}_{1},1)}}{,\ \ }\ldots{,\ \ }{\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath z}}}{{\mbox{\fraknomath z}}}{{\mbox{\scriptscriptscriptfrak z}}}{{\mbox{\scriptscriptscriptfrak z}}}_{\,\mathchoice{{\mbox{\fraknomath\char 141\relax}}}{{\mbox{\fraknomath\char 141\relax}}}{{\mbox{\scriptscriptscriptfrak\char 141\relax}}}{{\mbox{\scriptscriptscriptfrak\char 141\relax}}}},1)}}$

in a limited number of steps.   Moreover,  for these relations,  there is a general procedure given by the initial proof that  ${\mathchoice{{\mbox{\fraknomath A}}}{{\mbox{\fraknomath A}}}{{\mbox{\scriptscriptscriptfrak A}}}{{\mbox{\scriptscriptscriptfrak A}}}{(\mathchoice{{\mbox{\fraknomath m}}}{{\mbox{\fraknomath m}}}{{\mbox{\scriptscriptscriptfrak m}}}{{\mbox{\scriptscriptscriptfrak m}}},1)}}$  holds for arbitrary m.

This way of justifying the extended form of mathematical induction with universal sentences as premises,  however,  is not applicable in general.  In particular,  one of the difficulties that may arise here is the circumstance that such extended inductions can be nested into each other in a complicated way.  Let us discuss a typical case of this kind in more detail.  We will deal here with a part of  Cantor’s theory of transfinite ordinal numbers that can be treated constructively.    |35

With the previous paragraph ends our excerpt presenting ď 3 of our typescript in total — here together with its English translation on the right-hand side pages (i.e. those with uneven numbers).

The original text suddenly breaks off here.  It is not clear whether the remainder is just incorrectly filed or whether \bernaysplain further draft (in GabelŊberger shorthand?)— which must have been written before the introduction to this subsection fragment — was never put into typewriting.

3 Trying to Find Hints on the Time of Writing

3.1 ď 1 of  Our Typescript

(Hints: Before 1929, 1931, or 1951–1977)

3.1.1 Possible explanations for the missing of the two paragraphs

on the “existential form” in the introductory part

To explain why the two paragraphs from the beginning of  ď 1 of  [?, ?; ?]  are missing in our typescript (as described in \sectrefsection Parallel introductory part),  we see the following three options:

The missing of the two paragraphs may indicate that our typescript was written before 1929 for the following reason:  Soon later the subject of these paragraphs, the “existential form”,   has become an integral part of the standard presentation, which was never dropped in publications;  cf. the initial sections of  [Bernays, 1930/31], [?, ?; ?]. 2. 2.

It could have been the case that \bernaysplain or the \hilbertplain school in logic temporarily dropped the idea of the “exiŊtentiale Form” after the shock of G*odel’s incompleteness theorems, say in 1931. 3. 3.

A third option is that the whole text was written by \hasenjaegernameplain during his stay as \bernaysplain’ assistant in Z*urich, or later as a consequence of this stay.  What speaks for this option is the overall improved pedagogical quality of our typescript as compared to the corresponding sections in [?, ?; ?].    Then these paragraphs may be not actually missing,  but just deferred to a later section where they are more appropriate from the pedagogical viewpoint.

3.1.2 The completely unknown introduction

In the completely unknown introduction to foundations of mathematics and \hilbertplain’s proof theory (cf. \sectrefsection A completely new introduction),  there are some references to relevant published work that may help to date our typescript.

There is the following reference (cf. Note 12, \sectrefsection A completely new introduction):

“Tatsachlich hat eŊ sich im Fall der BeweiŊtheorie herauŊgestellt, daȷ fur die gewunschten Nachweise der WiderspruchŊfreiheit formalisierter Theorien die finiten Methoden nicht zulanglich sind.”

“For the case of proof theory,  it has indeed turned out that the finitist methods are not sufficient for the desired proofs of consistency of formalized theories.”

We do not think that this could have been written before autumn 1930,  when G*odel’s incompleteness theorems [G*odel, 1931] became known.  If this is so,  then our typescript cannot have been written before autumn 1930,  which excludes the first option of the previous subsection. 2. 2.

Moreover, there is the reference to [?, ?; ?; ?; ?]  in Notes  10 and 13  of  \sectrefsection A completely new introduction.   Unless the notes on the extra pages (cf. \sectrefsection additional footnotes)  were added much later to our typescript than our typescript itself was originally written (which is very unlikely because the position markers of the footnotes are already part of our typescript),  this means that our typescript cannot have been written before 1951. 3. 3.

Furthermore, there is also the following reference (cf. Note 17, \sectrefsection A completely new introduction):

“Dabei ist inŊbesondere der Umstand mitbestimmend, daȷ neuerdingŊ die beweiŊtheoretischen Untersuchungen in einen engeren Kontakt getreten sind mit den allgemeinen Theorien der abŊtrakten Algebra und Topologie,  |14  so daȷ die AuŊsicht sich er*offnet, daȷ die beweiŊtheoretischen Methoden zu einem wirkungŊvollen HilfŊmittel in diesen Gebieten sich entwickeln.”

“A particular reason for this non-limitation is the fact that recently the proof-theoretic investigations have come into closer contact with the general theories of abstract algebra and topology,   |14  and thus the prospect is opening up that the proof-theoretic methods may develop into a powerful tool in these fields.”

We have no idea to which publication before [Hasenjaeger, 1950c]  the contact with topology could refer.

If our assessment in the last two items is correct,  then also the second option of the previous subsection can be excluded and our typescript was probably written by Hasenjaeger during or after his stay with \bernaysplain in Z*urich.

3.2 ď 2 of  Our Typescript

(Hints: Hasenjaeger, 1951–1977)

The sentence of our typescript found in the second instead of the first edition of “\grundlagendermathematiknoindex” (which we discussed in \sectrefsection A sentence following the second edition instead of the first one)  clearly speaks in favor of a version written during the preparation of the second edition;  and the only work in this context we know about is the joint work of Hasenjaeger and \bernaysplain.

The sentence of our typescript improving on both editions of “\grundlagendermathematiknoindex” (which we discussed in \sectrefsubsection A significant improvement compared to both editions)  makes it likely that it was written with the intentionof a thorough revision;  and the only such attempt we know about is the joint work of Hasenjaeger and \bernaysplain.   Moreover,  as \bernaysplain used to keep track of any correction very carefully in his author’s copies,242424Such as the one of the first edition [?, ?; ?] owned by Erwin Engeler and the one of the second edition [?, ?; ?] owned by René \bernaysplain, cf. [?, ?; ?; ?].  such an improvement over both editions strongly indicates that our typescript may be the result of a collaboration of Hasenjaeger and \bernaysplain after the publication of the second edition of the first volume (1968),  i.e. in the years from 1968 to 1977 (when \bernaysplain died).

3.3 ď 3 of  Our Typescript (No Hints)

Although ď 3  of our typescript is very interesting and we would be keen on reading the remainder of it if it were found,  it breaks off too soon for giving us a clear hint on the time of its writing.

4 Hasenjaeger and \bernaysplain

As we have seen,  for finding out the time of writing of our typescript,  it may be helpful to find out more about Hasenjaeger’s scholarship as \bernaysplain’ assistant in Z*urich for the preparation of the second edition of “\grundlagendermathematiknoindex” in the early 1950s (cf. \sectrefsection The Mentioning of the Given-Up Work on the Second Edition).  So the questions is: What do we know about the relation of Hasenjaeger and \bernaysplain around the year  1950 ?

Besides several biographical remarks from Hasenjaeger in [Menzler-Trott, 2001],  there seem to be essentially only two non-trivial biographical texts on Hasenjaeger:  One is a laudation by Diller [Diller, 2000];  the other one is on his time as a cryptologist responsible for the security of the German Enigma in the second world war and appears in similar forms in [?, ?; ?; ?].  There we learn that he was born \Jun 1, 1919, in HildeŊheim (Germany) as a son of a lawyer,252525According to [Menzler-Trott, 2001, p.186]  and also to Hasenjaeger’s daughter Beate Becker,  \hasenjaegernameplain’s father was Edwin Hasenjaeger (1888–1972),  who was the mayor of M*ulheim an der Ruhr (Germany) from 1936 to 1946,  and a very close friend of  Heinrich Scholz (according tohttps://www.muelheim-ruhr.de/cms/edwin_hasenjaeger_-_portrait_eines_oberbuergermeisters_1936-19461.html).  that he was seriously wounded on January 2, 1942, as a German soldier in Russia,  and that the famous logician, philosopher, and theologian Heinrich Scholz (1884–1956) saved him from being ordered to the Russian front again, by recruiting him for the cryptology department of the High Command of the German Armed Forces (OKW/Chi) in Berlin.

As we were neither able to find a reasonable short CV of Hasenjaeger in publications nor in the WWW,  we have put his own one and a further one compiled by us into our Appendix.  For a list of his publications, see our hint at the beginning of our Bibliography.

4.1 Early Relation

Hasenjaeger and \bernaysplain were exchanging letters on the first edition of “\grundlagendermathematiknoindex” since 1943,  and from 1949 on also on Hasenjaeger’s own work.262626In particular, Hasenjaeger and \bernaysplain were exchanging letters on the following publications: [?, ?; ?; ?; ?; ?].  They definitely met each other in autumn 1949 at the “Kolloquium zur Logistik und der mathematischen Grundlagenforschung”,   Sept. 27 – Oct. 1, 1949, Mathematisches ForschungŊinstitut Oberwolfach (MFO), Oberwolfach (Germany).  Indeed, the following photo272727Source: Univ. Archiv Freiburg (BreiŊgau, Germany): Depositalbestand E6. Scanned, imprinted, and usage permitted by Mathematisches ForschungŊinstitut Oberwolfach (MFO), Oberwolfach (Germany): https://opc.mfo.de/detail?photo_id=11199  shows Hasenjaeger in the back row to the right behind \bernaysplain (with H. Arnold Schmidt in dark suit to the right of \bernaysplain, and Kurt  Sch*utte rightmost):

\bernaysplain

seems to have reviewed the PhD thesis of  Hasenjaeger [Hasenjaeger, 1950c]  before May 24, 1950,  which is the date of the final report by Hasenjaeger’s supervisor Heinrich Scholz.282828For more information on Hasenjaeger’ promotion, see the item labeled [Hasenjaeger, 1950c] in our Bibliography.

4.2 Joint Work on “\grundlagendermathematiknoindex”

All in all,  three scholarships were granted to Hasenjaeger by the ETH  Board,292929In German: “ETH-Rat”,   at that time called “Schweizerischer Schulrat”.   For the grants see [?, ?; ?].  with the goal to assist \bernaysplain in the preparation of the second edition of “\grundlagendermathematiknoindex”.    Hasenjaeger’s first stay as \bernaysplain’ assistant in Z*urich took place in winter term 1950/51.303030Cf. [Hasenjaeger, 1950e].   As planned from the beginning,  a second stay followed in summer term 1951.

Only after this second stay in Zurich,  however,  Hasenjaeger produced the first proper sketch313131This sketch attached to [Hasenjaeger, 1951]  may only have been written in response to Scholz’ letter [Scholz, 1951a] to \bernaysplain,  where Scholz expresses his worries raised by an oral report from Hasenjaeger (who must have met Scholz in Munster between the years 1950 and 1951)  that the work on “\grundlagendermathematiknoindex” had not even started yet:“Inzwischen ist Herr Hasenjaeger hier erschienen, und ich habe ihn als allererte gefragt nach dem Stande der Arbeit an dem Grundlagenbuch. Er hat mir gesagt, dass diese Arbeit noch gar nicht hat anlaufen konnen, weil Sie die Mengenlehre erst fertig machen mussen. Die hat mich nun wirklich so erschreckt, dass ich es Ihnen mit der erten Moglichkeit sagen muss.”In English: “In the meantime,  Mr. Hasenjaeger appeared here,  and my very first question was about the state of affairs of the work on the foundations book.  He told me that this work could not even have started yet, because you first have to complete the set theory.  Now this has alarmed me to such an extent that I have to tell this to you with the first opportunity.”The noun phrase “the set theory” refers to [Bernays, 1954] (received \Mar 30, 1953),  where Hasenjaeger  is mentioned only in the form of a reference to [1953b].In the eyes of  Scholz,  it was even worse for Hasenjaeger’s career that the work of Hasenjaeger and \bernaysplain on the second edition did not even start before summer 1951,  cf. [?, ?; ?]. of the overall layout for the second edition of “\grundlagendermathematiknoindex”,   in the form of a rough table of contents.  This sketch was and still is attached to Hasenjaeger’s letter [Hasenjaeger, 1951]  to \bernaysplain.  It is an elaborated and augmented protocol of the first detaileddiscussion with \bernaysplain on the subject of the layout for the second edition of \hilbertplain–\bernaysplain,  which probably took place in Zurich at the very end of the summer term 1951.323232For estimating the time of the detailed discussion with \bernaysplain,  see also [Scholz, 1951d]  in addition to [Hasenjaeger, 1951].   In the letter [Hasenjaeger, 1951],  a very rough previous sketch is mentioned to have been brought into accordance with the elaborated sketch attached to [Hasenjaeger, 1951].  This very rough sketch is probably a protocol of a very first short discussion with \bernaysplain on the \hilbertplain–\bernaysplain subject,  which took place at the end of winter term 1950/51 in Z*urich.

During Hasenjaeger’s first two semesters in Zurich,  there were neither publications under his name nor work on the “\grundlagendermathematiknoindex”.    Therefore, a further stay of  Hasenjaeger as \bernaysplain’ assistant was strongly suggested by  Heinrich Scholz  already February 1, 1951,  in  Scholz’ letter [Scholz, 1951b]  to Hasenjaeger.   This third stay indeed took place during winter term 1951/52  at the ETH Zurich,  and Hasenjaeger left Zurich soon after February 18, 1952.333333Cf. [?, ?; ?].

Most surprisingly,  however,  this first proper sketch attached to [Hasenjaeger, 1951] does not show the slightest similarity with our typescript here.  As the non-matching of this sketch (handwritten by Hasenjaeger)  with our typescript is crucial for the timing assessment of our typescript,  let us quote the “Introduction” (“Einleitung”) right at the beginning of it, following the original line breaking:

“Die logische Struktur der mathematischen Theorien.

GliederungŊentwurf.

Einleitung (E)

1. a)

Endliche Bereiche. Das finite Schliessen in Bezug auf  “offene” Gesamtheiten(Spezies). Endliche Zahlen – OrdnungŊzahlen. Unendliche Bereiche. BeweisealŊ mathematische Objekte. 2. b)

Elementare VerbandŊ- und/oder Gruppen-theorie. Dabei Auf suchen der einfachsten SchlusŊweisen.  Auf stellung eineŊ provisorischen AuŊsagen-KalkulŊ (evtl. Dingvariablen zunachst nur als MitteilungŊzeichen; dann Ueberlegung zum) elementaren Kalk*ul mit freien Variablen. 3. c)

Kombinatorischer Reichtum der “BeweiŊtheorie”.    Einbettung der Beweis-theorie in die Zahlentheorie (Arithmetisierung).  ? Elementare Probleme,die nichtelementare Methoden erfordern;  Vergleich mit Zahlentheorie. 4. d)

WiderspruchŊfreiheit.  Behandlung durch endliche Modelle unddurch EntscheidungŊverfahren.  EntscheidungŊverfahren an sich (Beisp.Verb.theorie).”

English translation:

“The logical structure of mathematical theories.

Layout outline.

Introduction (E)

1. a)

Finite domains. Finitist inference w.r.t. “open” totalities (species). Finite numbers — ordinal numbers. Infinite domains. Proofs as mathematical objects. 2. b)

Elementary lattice and/or group theory. Thereby exploration of the most simple modes of inference.  Establishing a provisional propositional calculus (maybe object variables first only as symbols for communication; then considerations on the) elementary calculus with free variables. 3. c)

Combinatorial abundance of “proof theory”.    Embedding of proof theory into number theory (arithmetization).  ? Elementary problems that require non-elementary methods; comparison to number theory. 4. d)

Consistency.  Treatment by means of finite models and decision procedures.  Decision procedures themselves (example lattice theory).”

Moreover, this sketch attached to [Hasenjaeger, 1951]  shows that the goal of the joint work of Hasenjaeger and \bernaysplain was a complete rewriting or even a completely new writing of the book right from the beginning  —  definitely not just an integration of new parts into the first edition as found in our typescript and as indicated in the “Preface to the Second Edition”,   cf. \sectrefsection The Mentioning of the Given-Up Work on the Second Edition.

From the sequence of letters and postcards [Hasenjaeger, 1952e], [Bernays, 1952], [Hasenjaeger, 1952f],  it becomes clear that the project of a complete reorganization of the book was still continued in 1952;   in particular a completely new version of the treatment of the $\iota$-operator is discussed in this sequence of letters.   Moreover, Hasenjaeger’sstate-of-the-art introduction of the $\iota$-operator [Hasenjaeger, 1952h] — ready for press and fundamentally different from the obsolete treatment in both \hilbertplain–\bernaysplain editions — was probably already attached to the first letter [Hasenjaeger, 1952e].   Note that,  according to the sketch attached to [Hasenjaeger, 1951],  the $\iota$ was to be treated in Chapters VI and VII of all in all 12 chapters (incl. the unnumbered introduction and the supplement chapters).

All in all,  \bernaysplain* may give us a wrong impression*  by using the subjunctive  “erfordert hatte”  (“would have required”)  in the  “Preface to the Second Edition”,    cf. \sectrefsection The Mentioning of the Given-Up Work on the Second Edition.   Indeed,  as a complete rewriting of the book was obviously planned from the very beginning of the work in summer 1951 and pursued far beyond the end of Hasenjaeger’s last stay in Zurich in February 1952,  it cannot be the case that the planned work was reduced when— “already back then” when “Mr. G. Hasenjaeger came to Z*urich for some time” —“it became obvious that the integration of the many new results in the area of proof theory would have required a complete reorganization of the book.”   Of course,  \bernaysplain does not explicitly state that the work on a complete reorganization was reduced  “already back then”,    but his directly following sentence already speaks only of the reduced version of the second edition — without mentioning any other point in time for the decision on this reduction,  cf. \sectrefsection The Mentioning of the Given-Up Work on the Second Edition.   Considering \bernaysplain most contextual style of writing,  where a sentence often can only be understood correctly if the reader has the meaning of many sentences of the context completely in mind,343434 To the best of our knowledge,  the only German author who clearly tops Paul  \bernaysplain  in this aspect is Jean Paul.  we never had the slightest doubt on the identity of these two points in time for several decades,  until we started our investigations on the joint work of Hasenjaeger and \bernaysplain.

The truth about the joint work of  Hasenjaeger and \bernaysplain on the  “\grundlagendermathematiknoindex”  seems to be that this work was given up only after a completely reorganized version for the first volume was already written,  including two completely new chapters on the  $\iota$-operator (among other subjects).   Be reminded that the $\iota$-operator is treated in both published editions at the very end of the first volume only in a single chapter,  which does noteven meet the state of the art of the original treatment of the $\varepsilon$ in the first edition of 1939.

In addition to this huge work on the entire first volume,  the joint work of Hasenjaeger and \bernaysplain also includes the writing of our typescript (not at all following the “Introduction” presented above)  and, moreover, at least the still lost continuation of its ď 3.

5 Conclusion

5.1 Concluding Assessment of Our Typescript

In spite of some minor evidence that our typescript was written before 1929 (cf. \sectrefsection Parallel introductory part II(1))  or in the year 1931 (cf. \sectrefsection Parallel introductory part II(2)),  the overwhelming evidence says that it was written not before 1951 (as explicated in ďď  3.1.2 and 3.2).   In \sectrefsection Joint Work,  we then studied the joint work of \bernaysplain and Hasenjaeger in Z*urich 1950–1952,  where we found some further evidence that our typescript resulted from that joint work.   After all,  the strongest evidence we have is the following:  Two carbon copies of our typescript were found in Hasenjaeger’s legacy— together with the only source for the footnotes to our typescript!   As Hasenjaeger seems to have added these footnotes to a typescript corrected by \bernaysplain’ hand with marks indicating the places of the anchors for these footnotes,  Hasenjaeger must have been more or less involved in the production of our typescript — and,  for this and several other reasons (cf. ďď  2.1 and 2.2),  he is most probably the actual typist of it as well.

What we still do not know, however, is the time of writing,  and we cannot exclude any year from 1951 to 1968 (when the second edition of the first volume was published).  Because of the improvements of our typescript over both editions of \hilbertplain–\bernaysplain (cf. \sectrefsubsection A significant improvement compared to both editions, \sectrefsection Parallel introductory part II(3), \sectref2 of Our Typescript),  even the years from 1968 to 1977 (when \bernaysplain died) cannot be excluded.  Most likely, however, is the time of the winter term 1951/52,  the last one Hasenjaeger stayed with \bernaysplain at the ETH in Z*urich (as explicated in \sectrefsection Joint Work).

In any case,  the finding of this incorrectly filed typescript is essential in the context of \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”,   because it provides us with some new insights353535For instance,  ď 2 of our typescript has provided us with some new insight into the finitist standpoint, which helped us to improve the translation of the first part of  ď 2 of [?, ?; ?] in [Hilbert & Bernays, 2017a]  considerably,  cf. \sectrefsubsection A significant improvement compared to both editions.Moreover — and maybe more important — also ď 3 of our typescript has provided us with some new insight into the finitist standpoint, which led to Note 349.2 in [Hilbert & Bernays, 2017c, p. 349]. into the finitist standpoint and its development,  in particular in connection with the two editions of the first volume of “\grundlagendermathematiknoindex”  [?, ?; ?].

5.2 Three Most Interesting Scripts Still Missing

As we do not know any way to find the following three scripts with our limited resources, the treasure quest remains open for future prospectors:

It is worthwhile to invest further effort and to search the legacy of \bernaysplain and the ETH archives more broadly:  There may be a chance to find an incorrectly filed continuation of our typescript,  at least the remainder of its ď 3,  possibly in form of a draft partly in \bernaysplain’ GabelŊberger shorthand.

Such a finding may change our point of view on \bernaysplain’ ideas on the foundations of mathematics considerably. 2. 2.

Be aware that our typescript must not be mistaken for the other script  that Hasenjaeger wrote according to his handwritten sketch attached to [Hasenjaeger, 1951]  —  probably a typescript of a completely rewritten first volume of  “\grundlagendermathematiknoindex”,    cf. \sectrefsection Joint Work.

This other script would be a real bonanza regarding the views of \bernaysplain on the foundations of mathematics in the early 1950s.

We have no idea on the whereabouts of this other script.

It would be a real pity if this major work of Hasenjaeger and \bernaysplain,  which can hardly be overlooked in any library by its mere size,  really remained lost. 3. 3.

Finally,  to find the script for the first edition remains,  of course,  one of the biggest wishes of maybe every historian of modern logic.

Acknowledgments

We would like to thank Beate Becker (née Hasenjaeger), Ludwig \bernaysplain, Rainer Glaschick, Paolo Mancosu, Klaus Schmeh, and Wilfried Sieg for their most helpful comments, and Norbert Hungerb*uhler and Frieder Stolzenburg for their kind support.

Curriculum Vitae of \hasenjaegernameplain by Himself

German Original

The following is a reprint of [Hasenjaeger, 1997], written by \hasenjaegernameplain himself.  Also the layout is exactly the one of Hasenjaeger’s ASCII file.

Erstellt am: 16.08.1997

                VITA    Gisbert HASENJAEGER, geb. 01.06.19 Hildesheim

          [REM mit Korrekturen im Sinne von Standardisierung und von K*urzungen

               einverstanden; Mitteilung des Ergebnisses erbeten]

          1937 Abitur in M*ulheim a.d. Ruhr.1937-1939 Arbeits- und Wehr-dienst.

          1942 Nach "Kopfschuȷ" (2.1.) und Rekonvalensenz bei OKW/CHI gegen

               (wie ich viel sp*ater erfuhr) A. Turing eingesetzt.

          1945-1950 Studium in M*unster/Westf., dabei seit Beginn (wissensch.)

               Hilfskraft am Seminar/Institut f*ur Mathematische Logik und

               Grundlagenforschung.

          1950 Promotion zum Dr.rer.nat. bei Heinrich Scholz mit der Disser-

               tation "Topologische Untersuchungen zur Semantik und Syntax

               eines erweiterten Pradikatenkalkuls".

          1950 wissenschaflicher Assistent am o.a. Institut.

          1950/51 (das akademische Jahr) Stipendiat Gast bei Paul Bernays a.d.

               ETH Z*urich.

          1953 Habilitation und venia legendi (Mathematische Logik und Grund-

               lagenforschung) an der Universitat Munster (Habilitationsschrift.

               Widerspruchsfreie Axiomensysteme ohne Standard-Modell).

          1955 Diatendozentur, 1960 apl. Professur U Munster.

          1961 SS und WS 61/62 Vertretung einer neu gegrundeten Professur fur

               Logik an der Philosophischen Fakultat der Universitat Bonn.

          1962 Berufung auf diese (a.o.) Professur, f*ur Logik und Grundlagen-

               forschung. [REM Durch das Fehlen des Adjektivs (math.) und den

               heutigen Sprachgebrauch ist das nun wohl "ein weites Feld",

               welches zu beackern ich mir nicht mehr zumuten m*ochte.]

          1964 Pers*onlicher Ordinarius, 1966 o. Prof.

          1964/5 (das akademische Jahr) Gast am Institut for Advanced Studies

               Princeton N.J.

          1970/1 (das akademische Jahr) Gast-Professur an der University of

               Illinois in Urbana/Champaign.

          1984 Emeritierung U Bonn.

English translation

Date of Generation: Aug. 16, 1997

                VITA    Gisbert HASENJAEGER, born May 1, 1919, in HildeŊheim (Germany)

        [REM[ark?:] I agree with corrections in the sense of standardization and abbreviation,

                         but ask for communication of the result]

        1937 A-levels (Abitur) in M*ulheim a.d. Ruhr.

        1937–1939 Working and Military Service.

        1942 After shot in the head (\Jan 2) and reconvalensence at OKW/CHI

               mission against A. Turing (as I was told much later).

        1945–1950 Studies in M*unster/Westf., from the beginning Scientific Assistent at the

                       Seminar/Institute for Mathematical Logic and Foundational Research

        1950 Promotion to Dr.  rer.  nat. by Heinrich Scholz with the dissertation.

                “Topological Investigations on Semantics and Syntax of an Extended

                   Predicate Calculus”.

        1950 Postdoctoral Research Assistent at the above-mentioned institute.

        1950/51 (the academic year) Scholarship Awardee as a guest of Paul  \bernaysplain at the

                                              ETH Zurich.

        1953 Habilitation and venia legendi (mathematical logic and foundational research)

               at the Univ. M*unster

               (habilitation thesis: “Consistent Axiom Systems Without Standard Model”).

        1955 Position of Supernumerary University Lecturer, 1960 Adjunct Professor,

               Univ. M*unster

        1961/62  (summer and winter term)  Deputy for a newly founded logic professorship

                                                        at the philosophical faculty at Univ. Bonn.

        1962 Appointed to this professorschip, for logic and foundational research.

               [REM As the adjective “math.” is lacking here and according to today’s

                usage of language, this seems to be a “wide field” nowadays, which I

                would definitely not want to treat anymore.]

        1964 Personal Professor (“Pers*onlicher Ordinarius”),

        1966 Full Professor (“Ordinarius”).

        1964/5 (the academic year) Guest at the Institut for Advanced Studies

                                             Princeton N.J.

        1970/1 (the academic year) Guest Professorship at the Univ. of Illinois in

                                             Urbana/Champaign.

        1984 Professor Emeritus, Univ. Bonn.

Our Curriculum Vitae of \hasenjaegernameplain

To provide some more detail and to overcome errors in other publications, we carefully compiled the following Curriculum Vitae.363636Sources: Correspondence Hasenjaeger–\bernaysplain: [?, ?; ?; ?; ?].  Three Curricula Vitae by Hasenjaeger himself: [?, ?; ?; ?].  Published articles: [?, ?; ?; ?].  Unpublished laudation: [Diller, 2000].  Communication with \hasenjaegernameplain’s daughter Beate Becker by E-mail and by phone, \Jan–Feb. 2018 and \Jan 2020.

1919 Born in HildeŊheim (Germany), \Jun 1.

1937 A-levels (“Abitur”) in M*ulheim an der Ruhr (Germany).

1937–1939 Involuntary373737Contrary to a text that wrongly puts Hasenjaeger close to being an admirer of the Nazi reign of terror, found on Dec. 28, 2019, in the German, English and French Wikipedia entries on \hasenjaegernameplain and also in the many places that automatically copy this attack to the soundness of public knowledge, Hasenjaeger did not do these services voluntarily. For instance, in the German version we read: “Hasenjaeger war danach freiwillig beim Reichsarbeitsdienst und leistete seinen Wehrdienst.”Having completed his 18 th year by \Jun 1, 1937, Hasenjaeger was forced by law to do 6 months service according to the ReichŊarbeitŊdienstgesetz of \Jun 26, 1935, immediately followed by 24 months service according to the Wehrgesetz of May 21, 1935.  So he should have been drafted by the Nazi state by July 1937, unless something relevant for the Nazi regime spoke against it, such as activities relevant for warfare, which included studying medicine.  According to these laws, the length of these services are to be set by the “Fuhrer and ReichŊkanzler”,   i.e. by Adolf Hitler, who chose these times as given here.A possible source for the claim of a voluntary participation is a new link on \Jan 10, 2020, in the German Wikipedia, pointing to [Schmeh, 2005], where we read: “Nach dem Abitur im Jahr 1936 meldete er sich zunachst freiwillig zum Arbeitsdienst, um anschlieȷend studieren zu konnen. Da jedoch der Krieg dazwischen kam, wurde er zum Militardienst eingezogen.”  In [Schmeh, 2009, p. 343] we find an English version of these sentences: “After his graduation in 1936, he volunteered for labor service, planning to take up his studies afterwards. But the war intervened and he was drafted.”Several aspects should be noted here:  (1) The sentences are not very reliable as Hasenjaeger writes in his own CV [Hasenjaeger, 1997] that he graduated in 1937, which is perfectly in line with the German standard of entering school with 6 (i.e. in late summer 1925) and graduating 12 years later from 1937 on (before 1937: 13 years).  (2) The war intervened not during Hasenjaeger’s labor service, but during his later military service. (3) In [Schmeh, 2009, p. 343] we read: “The author met him in 2005, a year before his death.” Therefore, the German sentence in [Schmeh, 2005] is closer to the communication of Klaus Schmeh with Hasenjaeger in 2005 and therefore more reliable.  (4) This is relevant because the German version actually says something different: Not the labor service was voluntary, but his “Meldung” (“answer” or “notice”). Thus, after passing his obligatory muster (probably in late 1936), Hasenjaeger probably answered that he would prefer an early start of his labor service because he wanted to study mathematics (but not medicine!)  after his labor and military services without any interruption of his studies. Working and Military Service (ReichŊarbeitŊ- und Wehrdienst).

1939 Drafted for Military Service in World War II.

1941–1942 Artillerist in the German Attack of Russia (“Russlandfeldzug”).

1942 Shot through his helmet to the head as a German soldier in Russia, \Jan 2.

1942–1945 Cryptologist at the High Command of the German Armed Forces in Berlin.

1945–1950 Studies in Mathematics and Physics, Univ. of M*unster (Westfalen, Germany).

1945–1950 Scientific Assistant (“wissenschaftl. Hilfskraft”),  “Seminar/Institut f*ur

Mathematische Logik und Grundlagenforschung”  at the Univ. of M*unster.

1950 Promoted to Dr.  rer.  nat. (PhD) [Hasenjaeger, 1950c]

by Heinrich Scholz (1884–1956).

1950 Postdoctoral Research Assistant (“wissenschaftl. Assistent”),  “Institut f*ur

Mathematische Logik und Grundlagenforschung”  at the Univ. of M*unster.

1950–1952 Three Scholarships in winter term 1950/51, summer 1951, winter 1951/52,383838In his own CV [Hasenjaeger, 1997], Hasenjaeger omits the last semester of his grants in Zurich. In his draft for an English CV [Hasenjaeger, 1970], however, he writes: “From autumn 1950 to spring 1952 I worked under a scholarship with P. \bernaysplain at the ETH, Switzerland.” Up to now, we can only be certain that Hasenjaeger was in Zurich for the first 18 days of February 1952, i.e. during the very end of the winter term 1951/52, and that he planned to meet Scholz in Munster (Westfalen) not before Feb. 29, 1952. The hard evidence for this is the letter [Hasenjaeger, 1952d] to Scholz, written on Feb. 18, 2012, in Zurich.

granted by the ETH Board, for visiting the ETH Zurich to assist \bernaysplain

in the writing of the second edition of  “\grundlagendermathematiknoindex”.

1953 Habilitation [Hasenjaeger, 1953a],  and venia legendi (Mathematische

Logik und Grundlagenforschung)  at the University of M*unster.

1955–1960 Lecturer (“Diatendozentur”)  at the University of Munster.

1956 Married Irmhild Reinl*ander (a former student assistant of Scholz,

mathematics & physics teacher in Soest (Germany) 1955–1957, died 2012).

1957 Son AndreaŊ is born.

1959 Daughter Beate is born.

1960–1961 Associate Professor (“apl. Prof.”)  at the University of M*unster.

1961 Daughter Cordula is born.

1961–1962 Substitute Professor in summer term 1961 and winter term 1961/62

at a newly founded professorship for logic at the philosophical faculty

of the University of Bonn (Germany).

1962–1984 Associate Professor (“a. o. Prof.”) on this professorship,

“Pers*onlicher Ordinarius” 1964, Full Professor (“Ordinarius”) 1966.

Director of the newly founded “Seminar f*ur Logik und

Grundlagenforschung” at the University of Bonn.

1964–1965 Visitor at the Institute for Advanced Study, Princeton (NJ),

winter term 1964/65 and summer term 1965 (with his family).

1970–1971 Visiting Professor at the Univ. of Illinois at Urbana–Champaign

winter term 1970/71 and summer term 1971 (with his family).

1984–2006 Professor Emeritus at the University of Bonn.

2006 Died on the estate of his wife in Plettenberg (Germany), Sept. 2.

Index

• Achilles Paradox §2.4.2

• Ackermann, Wilhelm (1896–1962) §1.1

• Archimedes (28?–212(?) b.c.) §2.4.3, §2.4.3

• Autexier, Serge (*1971) Wirth &al., 2009, Wirth &al., 2014, Autexier, 2003

• Bauer-Mengelberg, Stefan (1927–1996) Hilbert, 1926, Hilbert, 1928, Löwenheim, 1915

• Becker, Beate (*1959) Bernays & Hasenjaeger, 1952(?), Hasenjaeger, 1997, footnote 2, footnote 25, footnote 36, §2.2, §2.2, Acknowledgments, Our Curriculum Vitae of \hasenjaegernameplain

• Becker, Oskar (1889–1964) Hasenjaeger, 1968a, Hasenjaeger & Thyssen, 1968

• Benzmüller, Christoph (*1968) Wirth &al., 2009, Wirth &al., 2014

• Berlin Hilbert, 1909, Hilbert, 1913, Hilbert, 1922, Hilbert, 1923, Hilbert, 1930b, Hilbert, 1932ff., Hilbert, 2004, Hilbert & Bernays, 1934, 1939, Hilbert & Bernays, 1968, 1970, Reid, 1970, Scholz, 1931, Scholz & Hasenjaeger, 1961, Börger, 1987, Börger &al., 1984, Fitting, 1990, Fitting, 1996, Hasenjaeger, 1950b, Hasenjaeger, 1952b, Hasenjaeger, 1958a, 1966a, 1966b, §4, Our Curriculum Vitae of \hasenjaegernameplain

• Bernays, Ludwig (1924–2020) Bernays, 2017, §2.1, Acknowledgments

• Bernays, Paul (1888–1977) Bernays, 1941a, Hilbert, 1899, Bernays, 1941b, Hilbert, 1956, Hilbert, 1956, Hilbert, 1962, Hilbert, 1962, Bernays, 1942a, Hilbert, 1968, Hilbert, 1968, Hilbert, 1972, Hilbert, 1972, Hilbert & Bernays, 1934, 1939, Hilbert & Bernays, 1968, 1970, Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Bernays, 1942b, Hilbert & Bernays, 2017c, Bernays, 1943, Bernays, 1948, Scholz, 1950, Scholz, 1951a, Bernays, 1952, Wirth, 2021, Bernays, 1954, Bernays, 1958, Bernays, 1976, Bernays, 1986, Bernays & Hasenjaeger, 1952(?), Hasenjaeger, 1950c, Hasenjaeger, 1950d, Hasenjaeger, 1950e, Hasenjaeger, 1951, Hasenjaeger, 1952e, Hasenjaeger, 1952f, Hasenjaeger, 1952h, Bernays, 2017, Bernays, 1930/31, Bernays, 1937, Bernays, 1938, footnote 31, footnote 32, footnote 34, footnote 36, footnote 38, footnote 4, §1.1, §1.2, §1.2, §1.2, §1.2.1, §1.2.2, §1.2.2, §2.1, §2.1, §2.1, §2.1, §2.2, §2.2, §2.2, §2.3, §2.3, §2.5.1, §2.6.1, item 2, item 3, §3.1.2, §3.2, §3.2, §4, §4, §4.1, §4.1, §4.2, §4.2, §4.2, §4.2, §4.2, §4.2, item 1, item 1, item 2, item 2, §5.1, §5.1, §5.1, Curriculum Vitae of \hasenjaegernameplain by Himself, English translation, Our Curriculum Vitae of \hasenjaegernameplain

• Bernays, René (*1949) footnote 24

• Bolzano, Bernard (1781–1848) §2.4.3, §2.4.3

• Boole, George (1815–1864) §2.4.3, §2.4.3

• Bourbaki, Nicolas (pseudonym) Bourbaki, 1939ff.

• Brouwer, L. E. J. (1881–1966) Brouwer &al., 1955, §1.1, §2.4.3, §2.4.3

• Cantor, Georg (1845–1918) §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.6.1, §2.6.1

• Cauchy, Augustin Louis (1789-1857) §2.4.3, §2.4.3

• completeness §2.4.3, §2.4.3

• problem of §2.4.3

• concept formation §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3

• consistency

• problem of §2.4.3

• contentual §2.4.3, §2.4.3, §2.4.3, §2.6.1

• Crossley, John N. (*1937) Crossley, 1967

• Dawson, John W., Jr. (*1944) G*odel, 1986ff., G*odel, 1986ff.

• decision procedure item d)

• Dedekind, Richard (1831–1916) §2.4.3, §2.4.3

• descente infinie Wirth, 2004

• Diller, Justus (*1936) Diller, 2000, §4

• Dreben, Burton (1927–1999) Herbrand, 1930, Herbrand, 1971

• Engeler, Erwin (*1930) footnote 24

• Eudoxos of Cnidus (ca. 408 BC – ca. 355 BC) §2.4.3, §2.4.3

• existential judgment footnote 9, item 2, item 2, §2.6.1

• Feferman, Solomon (1928–2016) G*odel, 1986ff.

• finitism §2.6.1

• finitist footnote 14, footnote 19, footnote 35, §1.1, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.5, §2.5, §2.5.2, §2.6, §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1, item 1, item 1, item a), §5.1

• Fraenkel, Adolf Abraham (1891–1965) Bernays, 1958

• Frege, Gottlob (1848–1925) §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3

• Gabbay, Dov (*1945) Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Hilbert & Bernays, 2017c, Gabbay & Woods, 2004ff.

• Gabelberger shorthand §2.6.1, item 1

• Gegenstand item 2

• Gentzen, Gerhard (1909–1945) Menzler-Trott, 2007, §1.1

• Glaschick, Rainer (*1949) Hasenjaeger, 1997, Acknowledgments

• Goeb, Margarethe (1892–1962) Hilbert, 1917b

• Gödel, Kurt (1906–1978) G*odel, 1930, G*odel, 1931, G*odel, 1962, G*odel, 1986ff., §1.1, §2.4.3, §2.4.3

• G*ottingen Anon, 1899, Hilbert, 1917a, Hilbert, 1917b, Patzig &al., 1977, Behnke & Hasenjaeger, 1955, Hasenjaeger, 1959, §1.1, §1.2

• Goldfarb, Warren (*1949) G*odel, 1986ff., Goldfarb, 1970, Herbrand, 1930, Herbrand, 1971

• Griss, George F. C. (1898–1953) Griss, 1946, Griss, 1950, Griss, 1951a, Griss, 1951b, Griss, 1951c, Griss, 1951d, footnote 10, footnote 13

• Grundlagen

• der Geometrie Hilbert, 1899, Hilbert, 1899, Hilbert, 1903, Hilbert, 1909, Hilbert, 1913, Hilbert, 1922, Hilbert, 1923, Hilbert, 1930b, Hilbert, 1956, Hilbert, 1962, Hilbert, 1968, Hilbert, 1972, §1.1

• der Mathematik Hilbert, 1928, Hilbert & Bernays, 1934, 1939, Hilbert & Bernays, 1968, 1970, Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Hilbert & Bernays, 2017c, Wirth, 2021, Bernays & Hasenjaeger, 1952(?), footnote 31, [A Most Interesting Draft for \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”

that never found its way into any publication,

and  two  CV of  \hasenjaegernameplain

](#id10.id1), [A Most Interesting Draft for \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”

that never found its way into any publication,

and  two  CV of  \hasenjaegernameplain

](#id11.id2), §1.2, §1.2.2, §2.5.2, §3.2, §3.2, §4, §4.1, §4.2, §4.2, §4.2, §4.2, §4.2, item 2, §5.1, Our Curriculum Vitae of \hasenjaegernameplain

• Hamburg Hilbert, 1928

• Hasenjaeger, Edwin (1888–1972) footnote 25

• Hasenjaeger, Gisbert (1919–2006) Schmeh, 2009, Scholz, 1951a, Scholz, 1951b, Scholz, 1951c, Scholz, 1951d, Scholz & Hasenjaeger, 1961, Wirth, 2021, Bernays & Hasenjaeger, 1952(?), Börger &al., 1984, Diller, 2000, Hasenjaeger, 1950a, Hasenjaeger, 1950b, Hasenjaeger, 1950c, Hasenjaeger, 1950d, Behnke & Hasenjaeger, 1955, Hasenjaeger, 1950e, Hasenjaeger, 1951, Hasenjaeger, 1952a, Hasenjaeger, 1952b, Hasenjaeger, 1952c, Hasenjaeger, 1952d, Hasenjaeger, 1952e, Hasenjaeger, 1952f, Hasenjaeger, 1952g, Hasenjaeger, 1952h, Hasenjaeger, 1953a, 1953b, Hasenjaeger, 1953/54, Hasenjaeger, 1955, Hasenjaeger, 1958a, Hasenjaeger, 1958b, Hasenjaeger, 1959, Hasenjaeger, 1961, Hasenjaeger, 1962, 1965, 1966a, 1966b, 1967, Hasenjaeger, 1968a, Hasenjaeger, 1968b, Hasenjaeger, 1968c, Hasenjaeger, 1970, Hasenjaeger, 1972a, Hasenjaeger, 1972b, Hasenjaeger, 1976a, Hasenjaeger, 1976b, Hasenjaeger, 1976c, Hasenjaeger, 1977, Hasenjaeger, 1978, Hasenjaeger, 1984a, Hasenjaeger, 1984b, Hasenjaeger, 1984c, Hasenjaeger, 1987, Hasenjaeger, 1990, Hasenjaeger, 1995, Hasenjaeger, 1997, Hasenjaeger, 1998, Hasenjaeger & Thyssen, 1968, footnote 2, footnote 25, footnote 36, footnote 37, §1.2.2, §1.2.2, §1.2.2, §2.2, §2.3, item 3, §3.1.2, §3.2, §3.2, §4, §4.2, §4.2, §4.2, §5.1, German Original, English translation

• Heidelberg footnote 5, footnote 6

• Heijenoort, Jean van (1912–1986) Hilbert, 1905, Hilbert, 1926, Hilbert, 1928, Löwenheim, 1915, Wirth, 2012, G*odel, 1986ff., Heijenoort, 1971, Herbrand, 1930, Herbrand, 1968, Herbrand, 1971

• Henkin, Leon (1921–2006) Henkin, 1949

• Herbrand, Jacques (1908–1931) Wirth &al., 2009, Wirth &al., 2014, Herbrand, 1930, Herbrand, 1968, Herbrand, 1971, §1.1

• Herbrand’s Fundamental Theorem Wirth, 2012, Wirth, 2014, footnote 14, §1.2

• Hermes, Hans (1912–2003) Hasenjaeger, 1950c, Hermes & Scholz, 1952

• Heyting, Arend (1898–1980) Brouwer &al., 1955, footnote 10, footnote 13, §1.1

• Hilbert, David (1862–1943) Hilbert, 1899, Hilbert, 1900a, 1900b, Hilbert, 1902, Hilbert, 1903, Hilbert, 1905, Hilbert, 1909, Hilbert, 1913, Hilbert, 1917a, Hilbert, 1917b, Hilbert, 1918, Hilbert, 1922, Hilbert, 1923, Hilbert, 1926, Hilbert, 1928, Hilbert, 1930a, Hilbert, 1930b, Hilbert, 1932ff., Hilbert, 1956, Hilbert, 1962, Hilbert, 1968, Hilbert, 1971, Hilbert, 1972, Hilbert, 2004, Hilbert & Bernays, 1934, 1939, Hilbert & Bernays, 1968, 1970, Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Hilbert & Bernays, 2017c, Wirth, 2021, Bernays, 1930/31, footnote 5, footnote 6, §1.1, §1.1, §1.1, §1.1, §1.1, §1.1, §1.2, §1.2.1, §1.2.1, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.6.1, §2.6.1, item 2, §3.1.2, §5.1

• Hungerbühler, Norbert (*1964) Acknowledgments

• impossibility proof §2.4.2

• individual variable footnote 19

• induction

• mathematical §2.6.1, §2.6.1, §2.6.1, §2.6.1, §2.6.1

• Induktion

• vollständige §2.6.1, §2.6.1, §2.6.1, §2.6.1

• intuitionism footnote 10, footnote 13, §1.1, §2.4.3, §2.4.3

• Jean Paul (pseudonym), *see *Richter, Johann Paul Friedrich

• Kleene, Stephen C. (1909–1994) G*odel, 1986ff.

• König, Julius (1849–1913) K*onig, 1914, footnote 5, footnote 6

• Kronecker, Leopold (1823–1891) §1.1

• Löwenheim, Leopold (1878–1957) Löwenheim, 1915

• L*owenheim–Skolem Theorem footnote 14

• Logitik §2.4.3

• Mancosu, Paolo (*1960) Mancosu, 1998, Bernays, 1930/31, Acknowledgments

• McGuinness, Brian Francis Waismann, 1967

• Meltzer, Bernard (1916(?)–2008) G*odel, 1962

• Menzler-Trott, Eckart (1953–2017) Menzler-Trott, 2001, Menzler-Trott, 2007

• Méray, Charles (1835–1911) footnote 3, footnote 4

• Molk, Jules (1857–1914) Pringsheim, 1904/07

• M*unster (Westfalen, Germany) Scholz, 1932/33, Scholz, 1951d, Börger &al., 1984, Anon, 1984, Anon, 1984, Hasenjaeger, 1950c, Hasenjaeger, 1953a, Hasenjaeger, 1953/54, Hasenjaeger, 1961, Heinekamp &al., 1990, footnote 31, footnote 38, English translation, Our Curriculum Vitae of \hasenjaegernameplain, Our Curriculum Vitae of \hasenjaegernameplain, Our Curriculum Vitae of \hasenjaegernameplain, Our Curriculum Vitae of \hasenjaegernameplain, Our Curriculum Vitae of \hasenjaegernameplain, Our Curriculum Vitae of \hasenjaegernameplain

• Nedo, Michael (*1940) Wittgenstein, 1994

• Neumann, John von (1903–1957) §1.1

• number theory §2.4.3, §2.4.3, §2.4.3, §2.5, §2.5, §2.6.1, item c)

• Paris 1900b, Monk, 1904–1919, Bourbaki, 1939ff., Herbrand, 1930, Herbrand, 1930

• Parsons, Charles (*1933) G*odel, 1986ff.

• Paul, Jean (pseudonym), *see *Richter, Johann Paul Friedrich

• Peano, Guiseppe (1858–1932) §2.4.3, §2.4.3, §2.4.3, §2.4.3

• Peckhaus, Volker (*1955) Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Hilbert & Bernays, 2017c

• Peirce, Charles S. (1839–1914) §2.4.3, §2.4.3

• premise §2.6.1, §2.6.1, §2.6.1

• Pringsheim, Alfred (1850–1941) Pringsheim, 1898, Pringsheim, 1904/07

• proof theory footnote 13, [A Most Interesting Draft for \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”

that never found its way into any publication,

and  two  CV of  \hasenjaegernameplain

](#id10.id1), [A Most Interesting Draft for \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”

that never found its way into any publication,

and  two  CV of  \hasenjaegernameplain

](#id11.id2), [A Most Interesting Draft for \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”

that never found its way into any publication,

and  two  CV of  \hasenjaegernameplain

](#id11.id2.10), §1.2, §1.2.1, §1.2.1, §1.2.2, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, §2.4.3, item 1, item 3, §3.1.2, item c), §4.2

• propostional calculus item b)

• Richter, Johann Paul Friedrich (1763–1825) footnote 34

• Rödding, Dieter (1937–1984) Börger, 1987, Börger &al., 1984

• Russell, Bertrand (1872–1970) Whitehead & Russell, 1910–1913, §2.4.3, §2.4.3, §2.4.3, §2.4.3

• Russell’s Paradox §1.1

• satisfiable footnote 13, §2.4.1, §2.4.2

• Schmeh, Klaus (*1970) Schmeh, 2005, Schmeh, 2009, Schmeh, 2013, footnote 37, Acknowledgments

• Schmidt, Friedrich Karl (1901–1977) §1.2.2, §1.2.2, §1.2.2

• Schmidt, Hermann Arnold (1902–1967) §4.1

• Scholz, Heinrich (1884–1956) Scholz, 1931, Scholz, 1932/33, Scholz, 1950, Scholz, 1951a, Scholz, 1951b, Scholz, 1951c, Scholz, 1951d, Scholz & Hasenjaeger, 1961, Anon, 1984, Hasenjaeger, 1950c, Hasenjaeger, 1952d, Hermes & Scholz, 1952, footnote 25, §1.2.2, §1.2.2, §4, §4.1, §4.2, English translation, Our Curriculum Vitae of \hasenjaegernameplain

• Schröder, Ernst (1841–1902) §2.4.3, §2.4.3

• Schütte, Kurt (1909–1998) §4.1

• Sieg, Wilfried (*1945) G*odel, 1986ff., Acknowledgments

• Siekmann, J*org (*1941) Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Hilbert & Bernays, 2017c

• Stolzenburg, Frieder (*1966) Acknowledgments

• Thyssen, Johannes (1892–1968) Hasenjaeger & Thyssen, 1968

• uniqueness §2.4.3

• universal judgment footnote 9, item 2, item 2, §2.6.1

• validity §2.4.1, §2.4.3, §2.6.1

• universal §2.4.2

• Weierstraæ, Karl (1815–1897) §2.4.3, §2.4.3

• Weyl, Hermann (1885–1955) §1.1

• Whitehead, Alfred North (1861–1947) Whitehead & Russell, 1910–1913, §2.4.3, §2.4.3, §2.4.3, §2.4.3

• Wirth, Claus-Peter (*1963) Hilbert & Bernays, 2017a, Hilbert & Bernays, 2017b, Hilbert & Bernays, 2017c, Wirth, 2004, Wirth, 2012, Wirth, 2014, Wirth, 2017, Wirth, 2021, Wirth &al., 2009, Wirth &al., 2014, Wirth & Stolzenburg, 2016, Bernays, 2017, §2.1

• Wittgenstein, Ludwig (1889–1951) Waismann, 1967, Wittgenstein, 1994, §1.1

• Z*urich (Switzerland) Hilbert, 1918, Scholz, 1950, Bernays, 1952, Bernays, 1986, Bernays & Hasenjaeger, 1952(?), Gonseth, 1941, Hasenjaeger, 1950d, Hasenjaeger, 1950e, Hasenjaeger, 1951, Hasenjaeger, 1952e, Hasenjaeger, 1952f, Hasenjaeger, 1952h, Bernays, 1938, footnote 32, footnote 38, [A Most Interesting Draft for \hilbertplain and \bernaysplain’ “\grundlagendermathematiknoindex”

that never found its way into any publication,

and  two  CV of  \hasenjaegernameplain

](#id11.id2.16), §1.2.2, §1.2.2, §1.2.2, §2.1, item 3, §3.1.2, §4, §4.2, §4.2, §4.2, §4.2, §5.1, §5.1, German Original, English translation, Our Curriculum Vitae of \hasenjaegernameplain