David Hilbert (1862-1943) is one of the most outstanding representatives of mathematics, mathematical physics, and logic-oriented foundational sciences in general. 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'.

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:

*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.

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 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 epsilon, some kind of syntactic choice operator ....

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. 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 epsilon. 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 epsilon.