4
$\begingroup$

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.

$\endgroup$
3
  • 3
    $\begingroup$ Simpson’s book. $\endgroup$ Mar 24, 2015 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$ Mar 24, 2015 at 21:17
  • 3
    $\begingroup$ Emil is right about Simpson's book. In more detail: Stephen G. Simpson, "Systems of Second-Order Arithmetic" $\endgroup$ Mar 24, 2015 at 22:18

1 Answer 1

6
$\begingroup$

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.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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