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.

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

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:


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.