 Proof theory has become a large subject with many specialized branches that can be mathematically quite complex. So we have tried to present developments close to the main artery of its body, starting with its inception at the beginning of the twentieth century and ending with results from the close of the century. The theorems mentioned at the end of section 5 foreshadow investigations in the twenty-first century that are presented in Rathjen (2018) and concern relationships between Feferman’s systems of explicit mathematics and Martin-Löf type theories; the paper touches also on the completely new developments of homotopy type theory (see Awodey 2012). Some additional contemporary proof theoretic developments are described in appendices  D,  E and  F.  The theme of  Appendix E,  the extraction of computational information from proofs in particular formal theories, is the central topic of Schwichtenberg and Wainer’s 2012. They deal with theories of arithmetic and analysis up to \((\Pi^1_1{\Hy}\bCA)_0\). Standard texts on proof theory covering ordinal analysis are Takeuti 1985 and Schütte 1977. First steps into ordinal analysis are taken in Pohlers 2009. Finally, some new directions of proof theoretic work are taken in contributions to both Kahle and Rathjen 2015 and Jäger and Sieg 2018.