A hierarchy of ramified theories below primitive recursive arithmetic

The arithmetical theory EA(I;O) developed by Çagman, Ostrin and Wainer ([18] and [48]) provides a formal setting for the variable separation of Bellantoni-Cook predicative
recursion [6]. As such, EA(I;O) separates variables into outputs, which are quantified over, and inputs, for which induction applies. Inputs remain free throughout giving
inductions in EA(I;O) a pointwise character termed predicative induction. The result of this restriction is that the provably recursive functions are the elementary functions. An infinitary analysis brings out a connection to the Slow-Growing Hierarchy yielding є0 as the appropriate proof-theoretic ordinal in a pointwise sense. Chapters 1 and 2 are devoted to an exposition of these results.

In Chapter 3 a new principle of �1-closure is introduced in constructing a conservative extension of EA(I;O) named EA1. This principle collapses the variable separation in
EA(I;O) and allows quantification over inputs by acting as an internalised ω-rule. EA1 then provides a natural setting to address the problem of input substitution in ramified
theories.

Chapters 4 and 5 introduce a hierarchy of theories based upon alternate additions of the predicative induction and ∑1-closure principles. For 0 < k є N, the provably recursive
functions of the theories EAk are shown to be the Grzegorczyk classes Ek+2. Upper bounds are obtained via embeddings into appropriately layered infinitary systems with carefully controlled bounding functions for existential quantifiers. The theory EA-ω, defined by closure under finite applications of these two principles, is shown to be equivalent to primitive recursive arithmetic. The hierarchy generated may be considered
as an implicit ramification of the sub-system of Peano Arithmetic which restricts induction to ∑1-formulae.