As the authors say in the introduction, much of the results of this paper will look familiar to proof theorists. They include basic properties of functions and functionals defined by transfinite recursion, connection of Grzegorczyk and Hardy hierarchies and ordinal estimates for provably recursive functions and well-orderings of the systems with some forms of mathematical and transfinite induction. The emphasis is on detailed and careful proofs, and some refinements, like construction of a primitive recursive cut-elimination operator, are sacrificed.