The ramified theory of types allowed Feferman and Schutte to start from a relatively weak predicative theory $ACA_0$ which was conservative over first-order $PA$, and move to a much stronger predicative theory like $ATR_0$, as I discuss in this question. It similarly allowed Burgess and Hazen to start from Edward Nelson's theory, which was not much stronger than bounded arithmetic, and move to exponential function arithmetic, as I discuss in this question.

The ramified theory of types allowed Feferman and Schutte to start from a relatively weak predicative theory $ACA_0$ which was conservative over first-order $PA$, and move to a much stronger predicative theory like $ATR_0$, as I discuss in this question. It similarly allowed Burgess and Hazen to start from Edward Nelson's theory, which was not much stronger than bounded arithmetic, and move to exponential function arithmetic, as I discuss in this question.

EDIT: I haven't read it, but this chapter from Skolem's book "Abstract Set Theory" may be useful.