The hierarchies of theories Si2 and T i 2 of Bounded Arithmetic were defined

by Buss [1], for i ≥ 1 they are closely related to computational complexity classes in the polynomial time hierarchy. The theories S02 and T 0 2 allow induction on binary notation, resp. suc-cessor induction only for sharply bounded formulas, i.e., formulas in which every quantifier is bounded by a logarithmic term. The theory S02 was shown to be pathologically weak by Takeuti [3], and it was generally believed that T 02 was likewise weak. The paper under review studies the theory T 02 in the language of Bounded Arithmetic extended by a function symbol for MSP (x, i) = bx/2ic. This function gives access to the binary representation of numbers, so the ex-tended language is very natural and frequently used in the context of Bounded Arithmetic. The reviewer [2] has shown that S02 in this extended language is still weak. In this paper it is shown that T 02 in this language is surprisingly strong: it allows to define all polynomial time computable functions, and proves in-duction for sharply bounded formulas containing function symbols for these. Hence PV1, the universal theory of polynomial time computable functions, is a conservative extension of T 02