Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$?

2012-12-04T03:18:33Z

$\Pi^1_{\infty}\text{-}\mathsf{CA}_0$ proves existence of models of ATR$_0$. But I think it does not imply ATR$_0$, because Axiom Beta is a kind of replacement axiom. Is that right?

Answer by François G. Dorais for Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$?

2012-12-04T03:43:25Z

Yes, in fact $\Pi^1_1$-CA₀ suffices to prove ATR₀. The simplest way to see this is that ATR₀ is equivalent to $\Sigma^1_1$-separation: if $\phi(n)$ and $\psi(n)$ are $\Sigma^1_1$ formulas then $$\forall n (\lnot \phi(n) \lor \lnot\psi(n)) \rightarrow \exists C \forall n ((\phi(n) \rightarrow n \in C) \land (\psi(n) \rightarrow n \notin C)).$$ Assuming $\Pi^1_1$-CA₀ one can simply take $C = \lbrace n : \lnot\psi(n)\rbrace$, for example, to satisfy the conclusion. Details can be found in Simpson's Subsystems of Second-Order Arithmetic.

Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? - MathOverflow

Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$?

Answer by François G. Dorais for Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$?