 The main part of our article covers these exciting investigations for an expanded Hilbert Program through 1999—with special, detailed attention to results and techniques that by now can be called “classical” and are of continued interest. Newer, but still closely connected developments are sketched in Appendices: the proof theory of set theories in Appendix D, combinatorial independence results in Appendix E, and provably total functions in Appendix F. Here (infinitary) sequent calculi and suitable systems of ordinal notations are crucial proof theoretic tools. However, we discuss in section 4.2 also Gödel’s Dialectica Interpretation and some of its extensions as an alternative for obtaining relative consistency proofs and describe in section 5.2.1 the systematic attempt of completing the incomplete through recursive progressions. Both topics are analyzed further in Appendix C.2 and Appendix B, respectively. To complete this bird’s eye view of our article, we mention that the Epilogue, section 6, not only indicates further proof theoretic topics, but also some directions of current research that are connected to proof theory and of deep intrinsic interest. We have tried to convey the vibrancy of a subject that thrives on concrete computational and (meta-) mathematical work, but also invites and is grounded in general philosophical reflection.