 A second omission concerns Bounded Arithmetic, where feasibility issues are a central focus: one studies formal theories with provably recursive functions that form very small subclasses of the primitive recursive ones. Indeed, the class of the provably total functions of Buss’ base theory is that of functions that can be computed in polynomial time, and there was the hope that proof theoretic investigations might contribute novel results in complexity theory. A third omission concerns proof mining; that line of deep mathematical investigations using proof theoretic tools was initiated by Kreisel (1958, 1982) and Luckhardt (1989), but really perfected only by Kohlenbach (2007). We hinted at the work of his school at the very end of  section 4.1.