We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.]).

We survey a selection of results about majorization hierarchies. The main focus is on classical and recent results about the comparison between the slow and fast growing hierarchies.

Let T(Ω) be the ordinal notation system from Buchholz-Schütte (1988). [The order type of the countable segmentT(Ω)0 is — by Rathjen (1988) — the proof-theoretic ordinal the proof-theoretic ordinal ofACA 0 + (Π 1 l −TR).] In particular let ↦Ω a denote the enumeration function of the infinite cardinals and leta ↦ ψ0 a denote the partial collapsing operation on T(Ω) which maps ordinals of T(Ω) into the countable segment TΩ 0 of T(Ω). Assume that the (fast growing) extended Grzegorczyk (...) hierarchy $(F_a )_{a \in T(\Omega )_0 }$ and the slow growing hierarchy $(G_a )_{a \in T(\Omega )_0 }$ are defined with respect to the natural system of distinguished fundamental sequences of Buchholz and Schütte (1988) in the following way: $$\begin{array}{*{20}c} {G_0 (n): = 0,} & {F_0 (n): = (n + 1)^2 ,} \\ {\begin{array}{*{20}c} {G_{a + 1} (n): = G_a (n) + 1,} \\ {G_l (n): = G_{l[n]} (n),} \\ \end{array} } & {\begin{array}{*{20}c} {F_{a + 1} (n): = \underbrace {F_a (...F_a }_{n + 1 - times}(n)...),} \\ {F_l (n): = F_{l[n]} (n),} \\ \end{array} } \\ \end{array}$$ wherel is a countable limit ordinal (term) and (l[n]) n ∈N is the distinguished fundamental sequence assigned tol. For each ordinal (term)a in T(Ω) and each natural numbern letC n (a) be the formal term which results from the ordinal terma by successively replacing every occurence ofψ a by $\psi _{ - 1 + C_n (a)}$ whereψ −1 is considered as a defined function symbol, namely $\psi _{ - 1} b: = F_{\psi _0 b + 1} (n + 1)$ . (Note thatψ a 0=Ω a ) In this article it is shown that for each ordinal termψ 0 a in T(Ω) there exists a natural numbern 0 such thatψ 0 C n (a) ∈ T(Ω) and $G_{\psi _0 a} (n) \leqslant F_{\psi _0 C_n (a) + 1} (n + 1)$ holds for alln≥n 0. This hierarchy comparison theorem yields a plethora of new results on nontrivial lower bounds for the slow growing ordinals — i.e. ordinals for which the slow growing hierarchy yields a classification of the provably total functions of the theory in question — of various theories of iterated inductive definitions (and subsystems ofKPi) and on the number and size of the subrecursively inaccessible ordinals — i.e. ordinals at which the extended Grzegorczyk hierarchy and the slow growing hierarchy catch up — below the proof-theoretic ordinal ofACA 0+(Π 1 l −TR). In particular these subrecursively inaccessibles ordinals are necessarily of the form $\psi _0 \Omega ..._{\Omega _\omega }$. (shrink)

We give a term rewriting characterization of the polyspace functions. Our work follows investigations on term rewriting characterizations of some classes of (sub-) recursive functions as initiated by Cichon and Weiermann [4] and continued by Beckmann and Weiermann [1].The main novelty of this paper is a technique for reformulating recursion schemes. The aim of this technique is to provide rewriting rules which give rise to rewriting chains whose terms are suitably bounded. This bounding is crucial when dealing with computational classes (...) with space constraints. (shrink)

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)