$\mathsf{IR}$ and $\mathsf{ATR}_0$

In his first major work on systems of predicative analysis [3,4], Feferman introduces the system $\mathsf{IR}$ and proposes it as an explication of predicative provability.

``Although we strongly believe that the explications proposed in this paper for the notion of predicative provability in analysis are correct, we are not convinced that the matter has been settled conclusively by the results obtained so far. It is premature to say just what would constitute final evidence concerning this question. We expect that this will be revealed, at least in part, by further study of the theories considered here.'' (page 29)

In subsequent papers on predicative provability, Feferman does not back away from this proposal. The systems that he introduces in [5,6,7] as explications of predicative provability are conservative over $\mathsf{IR}$.

In this paper I want to compare Feferman's system $\mathsf{IR}$[3,4] with another subsystem of second order arithmetic $\mathsf{ATR}_0$ due to Friedman [9]. We begin by briefly reviewing the definitions of these systems.