# Formal definition of arithmetic transfinite recursion

Recently I have been trying to find the definition of the subsystem $ATR_0$ of second-order arithmetic. Only "definitions" I have found were quite vague, like informal definition on Wikipedia which says it's $ACA_0$ plus statement that "any arithmetical functional can be iterated transfinitely along any countable well ordering starting with any set", or some paper claiming that $ATR_0$ is just $ACA_0$+"for every ordinal $\alpha<\omega_1^\text{CK}$ $\emptyset^{(\alpha)}$ exists". Can anyone point me to the formal definition of this system?

• Simpson’s book. – Emil Jeřábek Mar 24 '15 at 21:15
• Though if you want a simple formula, the Wikipedia article mentions that it is equivalent to $\mathrm{ACA}_0 + \Sigma^1_1$-separation. – Emil Jeřábek Mar 24 '15 at 21:17
• Emil is right about Simpson's book. In more detail: Stephen G. Simpson, "Systems of Second-Order Arithmetic" – Andreas Blass Mar 24 '15 at 22:18

This first chapter also has information about Emil's comment about $\Sigma^1_1$-separation as well as some reverse math type equivalences, e.g. $\mathsf{ATR}_0$ is equivalent over $\mathsf{RCA}_0$ to the theorem that any two countable well orderings are comparable.