In this article we give a unifying approach to the theory of fundamental sequences and their related Hardy hierarchies of number-theoretic functions and we show the equivalence of the new approach with the classical one.

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

Let T be the standard Veblen 1908 ordinal notation system for Γ0 as defined, for example, in Schütte's 1977 textbook [13] on Proof Theory. We define a slight modification of the standard assignment of fundamental sequences for the limit ordinals in T and prove that Γ0 is subrecursively inaccessible for this assignment, i.e. the induced slow and fast growing hierarchy match up at Γ0 for the first time.The results of this paper also indicate that φε00 may be considered as a (...) new slow growing ordinal of PA in the sense that the induced slow growing hierarchy up to φε00 classifies the PA-provablyrecursive functions.We show how the results of this paper can be used to bui d a subrecursive hierarchyover the predicative ordinals in the spirit of Wainer's 1970 abstract [16 ]. (shrink)

In this, journal, W. Buchholz gave an elegant proof of a characterization theorem for provably total recursive functions in the theory IDv for the v-times iterated inductive definitions . He characterizes the classes of functions by Hardy functions. In this note we will show that a slow growing analogue to the theorem can be obtained by a slight modification of Buchholz' proof.