$\Pi^1_{\infty}\text{}\mathsf{CA}_0$ proves existence of models of ATR$_0$. But I think it does not imply ATR$_0$, because Axiom Beta is a kind of replacement axiom. Is that right?
Take the 2minute tour
×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Yes, in fact $\Pi^1_1$CA_{0} suffices to prove ATR_{0}. The simplest way to see this is that ATR_{0} is equivalent to $\Sigma^1_1$separation: if $\phi(n)$ and $\psi(n)$ are $\Sigma^1_1$ formulas then $$\forall n (\lnot \phi(n) \lor \lnot\psi(n)) \rightarrow \exists C \forall n ((\phi(n) \rightarrow n \in C) \land (\psi(n) \rightarrow n \notin C)).$$ Assuming $\Pi^1_1$CA_{0} one can simply take $C = \lbrace n : \lnot\psi(n)\rbrace$, for example, to satisfy the conclusion. Details can be found in Simpson's Subsystems of SecondOrder Arithmetic. 

