witnBo(~,s)(fo(~, C-),C-), . . < win, En-1) for appropriate functions fo, f 2 , . . , fl. If B1 C E~_2 then Wit~Bo is just Bo and Wit~B1 is just B1; and a single 3 :right inference applied to (4)gives wit l . . , - - ~ w i tnBl ( f l ( C, c-) , c-) , .

Win, E0), which in turn is equivalent to LOP(-< w~, El/. < wm least ordinal principle for primitive recursive predicates. < win, E,_I); since m >_ 2 always holds, these theories can prove the usual induction and least number principles for primitive recursive predicates, which is sufficient for formalizing all the metamathematical constructions in section 3. PROPOSITION 2 Let n > 1. ) - + TI( , P r o o f It is clear that IEn -= IA0 + TI(w, En) and by standard techniques these are equivalent to IIIn and IA0 + TI(w, IIn).