  We consider extensions of the language of Peano arithmetic by transfinitely
iterated truth definitions satisfying uniform Tarskian biconditionals. Without
further axioms, such theories are known to be conservative extensions of the
original system of arithmetic. Much stronger systems, however, are obtained by
adding either induction axioms or reflection axioms on top of them. Theories of
this kind can interpret some well-known predicatively reducible fragments of
second-order arithmetic such as iterated arithmetical comprehension.
  We obtain sharp results on the proof-theoretic strength of these systems
using methods of provability logic. Reflection principles naturally define
unary operators acting on the semilattice of axiomatizable extensions of our
basic theory of iterated truth. The substructure generated by the top element
of this algebra provides a canonical ordinal notation system for the class of
theories under investigation.
  Using these notations we obtain conservativity relationships for iterated
reflection principles of different logical complexity levels corresponding to
the levels of the hyperarithmetical hierarchy, i.e., the analogs of Schmerl's
formulas. These relationships, in turn, provide proof-theoretic analysis of our
systems and of some related predicatively reducible theories. In particular, we
uniformly calculate the ordinals characterizing the standard measures of their
proof-theoretic strength, such as provable well-orderings, classes of provably
recursive functions, and $\Pi_1^0$-ordinals.
