Spoors, Elliott John (2010) A hierarchy of ramified theories below primitive recursive arithmetic. PhD thesis, University of Leeds.

Text
Spoors_EJ_Department_of_Pure_Mathematics_PhD_2010.pdf Available under License Creative Commons AttributionNoncommercialShare Alike 2.0 UK: England & Wales. Download (638Kb) 
Abstract
The arithmetical theory EA(I;O) developed by Çagman, Ostrin and Wainer ([18] and [48]) provides a formal setting for the variable separation of BellantoniCook 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 SlowGrowing Hierarchy yielding є0 as the appropriate prooftheoretic ordinal in a pointwise sense. Chapters 1 and 2 are devoted to an exposition of these results. In Chapter 3 a new principle of �1closure 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 ∑1closure 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 subsystem of Peano Arithmetic which restricts induction to ∑1formulae.
Item Type:  Thesis (PhD) 

Academic Units:  The University of Leeds > Faculty of Maths and Physical Sciences (Leeds) > School of Mathematics (Leeds) > Pure Mathematics (Leeds) 
Depositing User:  Ethos Import 
Date Deposited:  23 Jun 2011 13:04 
Last Modified:  07 Mar 2014 11:23 
URI:  http://etheses.whiterose.ac.uk/id/eprint/1554 