Transfinite induction within Peano arithmetic Original Research Article

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.