Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-18T06:13:49Z http://mathoverflow.net/feeds/question/115351 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/115351/does-pi1-infty-comprehension-imply-atr-0 Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? Colin McLarty 2012-12-04T03:18:33Z 2012-12-04T03:43:25Z <p>$\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?</p> http://mathoverflow.net/questions/115351/does-pi1-infty-comprehension-imply-atr-0/115354#115354 Answer by François G. Dorais for Does $\Pi^1_{\infty}$ comprehension imply ATR$_0$? François G. Dorais 2012-12-04T03:43:25Z 2012-12-04T03:43:25Z <p>Yes, in fact $\Pi^1_1$-CA<sub>0</sub> suffices to prove ATR<sub>0</sub>. The simplest way to see this is that ATR<sub>0</sub> 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<sub>0</sub> one can simply take $C = \lbrace n : \lnot\psi(n)\rbrace$, for example, to satisfy the conclusion. Details can be found in Simpson's <em>Subsystems of Second-Order Arithmetic</em>.</p>