Transfinite induction within Peano arithmetic
Richard Sommer · Annals of Pure and Applied Logic · 1995
The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than ε0, and formulas restricted in quantifier complexity, is determined. This is done, in part, by describing the provably recursive functions of such theories. Upper bounds for the provably recursive functions are obtained using model-theoretic techniques. A variety of additional results that come as an application of such techniques are mentioned.