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?


Thanks in advance.



Formal definition of arithmetic transfinite recursion
To repeat Emil and Andreas's comments, it can be found in Stephen G. Simpson, "Systems of Second-Order Arithmetic", the first chapter of which is available here:


<http://www.personal.psu.edu/t20/sosoa/chapter1.pdf>


See Definition I.11.1 (p. 39, which is in the first chapter).


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.


