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.

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ Simpson’s book. $\endgroup$
    – Emil Jeřábek
    Commented 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$
    – Emil Jeřábek
    Commented 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$
    – Andreas Blass
    Commented Mar 24, 2015 at 22:18

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .