Grundlagen der Mathematik. I / Foundations of mathematics. I. Part A. Prefaces and §§1–2. Edited and with a preface by Dov Gabbay, Michael Gabbay, Jörg Siekmann and Claus-Peter Wirth. Commented translation by Claus-Peter Wirth of the second German edition of 1968, including the annotation and translation of all deleted parts of the first German edition of 1934. With a chapter “Hilbert’s proof theory” by Wilfried Sieg. Dual English-German text. (German, English) Zbl 1283.03005

Hilbert, David; Bernays, Paul

London: College Publications (ISBN 978-1-84890-033-2). lxiii, 170 p. (2011).

From the preface: David Hilbert (1862–1943) is one of the most outstanding representatives of mathematics, mathematical physics, and logic-oriented foundational sciences in general [C. Reid, Hilbert. With an appreciation of Hilbert’s mathematical work by Hermann Weyl. Berlin etc.: Springer (1970; Zbl 0192.32601)]. From the end of the 19th century to the erosion of the University of Göttingen by the Nazis, Hilbert formed and reshaped many areas of applied and pure mathematics. Most well-known and highly acknowledged are his Foundations of geometry [Grundlagen der Geometrie. Leipzig: Teubner (1899; JFM 30.0424.01)].
After initial work at the very beginning of the 20th century, Hilbert re-intensified his research into the logical foundations of mathematics in 1917, together with his new assistant Paul Bernays (1888–1977). Supported by Hilbert’s PhD student Wilhelm Ackermann (1896–1962), Hilbert and Bernays 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 object of number theory. The goal of Hilbert’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 intuitionistic movements of Leopold Kronecker (1823–1891), L. E. J. Brouwer (1881–1966), Herman Weyl (1885–1955), and Arend Heyting (1898–1980). The proof of the consistency of mathematics was to be achieved by sub-division into the following three tasks:
\(\bullet\) Arithmetization of mathematics.
\(\bullet\) Logical formalization of arithmetic.
\(\bullet\) 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 \(\overline A\).
The problematic step in this program (nowadays called Hilbert’s program) is the consistency proof.
We know today that Hilbert’s quest to establish a foundation for the whole scientific edifice could not be successful to the proposed extent: Gödel’s incompleteness theorems dashed the broader hopes of Hilbert’s program. Without the emphasis that Hilbert 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 sciences) would hardly have been achieved at his time.
The central and most involved presentation of Hilbert’s program and Hilbert’s proof theory is found in the two-volume monograph Grundlagen der Mathematik of Hilbert and Bernays [Vol. I. Berlin: Springer (1934; JFM 60.0017.02); Vol. II. Berlin: Springer (1939; JFM 65.0021.02)] to be presented here for the first time in English.
The first volume presents the motivation and philosophical foundation of Hilbert’s and Bernay’s original view on finitistic mathematics and their methodological standpoint for proof theory (§§1–2), a refined introduction to propositional and predicate logic (with equality) (§§3–5), and the consistency issues of a variety of (sub-) systems of number theory (including recursion theory, System (Z), and the elimination of the \(\iota\)-operator) (§§6–8).
The second volume of Grundlagen der Mathematik is focused on more advanced topics, such as a proof-theoretic sharpening of Gödel’s completeness theorem, a full argument for Gödel’s second incompleteness theorem, the demarcation of the finitistic standpoint, and especially, on Hilbert’s \(\varepsilon\), some kind of syntactic choice operator: Roughly speaking, ‘\({\varepsilon} x.\;A\)’ denotes some particular object \(x\) that renders the formula \(A\) as true, in the context of the free variables of \(A\), provided that there are such objects at all.
After the first edition of the Grundlagen der Mathematik had been out of print for a long period of time, Bernays prepared a revised second edition [D. Hilbert and P. I. Bernays, Grundlagen der Mathematik. I, 2. Auflage. Berlin: Springer (1968; Zbl 0191.28402); Grundlagen der Mathematik. II, 2. Auflage. Berlin: Springer (1970; JFM 65.0021.02)]. Beside small corrections, the second edition incorporated about a dozen multi-page new parts and some additional supplements; but about \(90\%\) of the pages were photo-identical to the first edition (except for the page numbers).
It has been a great impairment to science and foundational research that, although translations into Russian and French are available, there has never been an English edition of these two milestones in the development of modern mathematical logic. One of the reasons for the lack of a translation may have been the copyright issue, but a more important reason is certainly the enormous breadth of the required scholarship of the translators because of the deep insight displayed in the presented mathematical content, but also the very rich and sophisticated German language of the original, mixing philosophical and mathematical concepts and arguments, routed in more than one way in Kantian writings.
Although proof theory is nowadays well represented in excellent English textbooks and the further development of the field after World War II was published in English, and although Hilbert’s program and its related form of intuitionism (finitism) have been well documented and studied, the international research communities still lack access to the roots of proof theory, especially to the basic philosophical and epistemological conceptions of Bernays and Hilbert, as well as Hilbert’s \(\varepsilon\). The lack of access to the original sources has resulted in a simplistic and sometimes even mistaken evaluation of Hilbert’s proof theory, and especially of Hilbert’s \(\varepsilon\).

MSC:

03-03	History of mathematical logic and foundations
03-02	Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
01A75	Collected or selected works; reprintings or translations of classics
03B30	Foundations of classical theories (including reverse mathematics)
03Fxx	Proof theory and constructive mathematics

Citations:

Zbl 0192.32601; JFM 30.0424.01; JFM 60.0017.02; Zbl 0191.28402; JFM 65.0021.02