The Herbrand theorem shows that if an existential formula is provable, then so is a disjunction of substitution instances. The author first sharpens this condition to, for Herbrand theories, just one instance, and thus extracts a term t such that \(\phi\) (t) from a proof of \(\exists x\phi (x)\). Here, T(\({\mathfrak F})\) is said to be an Herbrand theory when it has QF(\({\mathfrak F})-IR\)- induction rule for quantifier-free formulas with function parameters from \({\mathfrak F}\)- where \({\mathfrak F}\) is closed under explicit definitions, definition by cases and bounded search. This is further sharpened for \(\exists \forall\)-formulas. [In this case a number of disjuncts are necessary.] He gives a number of interesting applications of these to the Grzegorczyk hierarchy, and the polynomial hierarchy [in bounded arithmetic of S. Buss et al.]. Here are two samples. (1) \(\Sigma^ 0_ 1({\mathfrak E})-IR\) is genuinely stronger than \(\Pi^ 0_ 1({\mathfrak E})-IR\), where \({\mathfrak E}\) is the Kalmar elementary class [Parsons]. (2) Elements of \({\mathfrak E}_ n\), \(n>2\), are exactly the functions provably total in \((\Pi^ 0_ 2({\mathfrak E})-IR)_{n-3}\), where the subscript indicates that the induction is applied at most n-3 times. The author's tool so far is nimble, and yet ``elementary'', transformations of proofs and extractions of relevant functions from proofs. By means of the same tool applied to second-order arithmetic, he gives a new proof of a Friedman's result that as to \(\Pi^ 0_ 2\)- formulas, PRA (primitive recursive arithmetic) is as strong as the second-order version of \(\Sigma^ 0_ 1-IR+\Sigma^ 0_ 1\)- AxCh\(+Weak\) König Lemma, among others. Towards the end of the paper, the author uses a more ``sophisticated'' method to prove powerful results like (a) QF(\({\mathfrak E}_{\infty})-IR+\Sigma^ 0_ 1-AC+\Pi^ 1_{\infty}-IR+WKL\) is conservative over (Hilbert's) Z, and (b) Provably total functions as of the second-order \(\Sigma^ 0_ n-IR\) are exactly the unnested \(<\omega_ n^{\omega}\)-recursive functionals. He first embeds the given proof in an infinitary system (with infinitary terms and the \(\omega\)-rule). This transformation is then formalized in the finitary system, and the reflection principle delivers the desired result. In the ``Concluding Remarks'', the author talks about possible directions of future research in proof theory.