In such a language an axiomatization of Tarski’s hierarchy of truth predicates can be formulated. On the proof-theoretic side iterating truth theories in the style of T(PA) corresponds to iterating elementary comprehension, that is, to iterating ACA. The system of iterated truth theories corresponds to the system of ramified analysis (see Feferman 1991). 