En $\Pi^1_{\infty}$ la comprensión implica ATR $_0$ ?

Question

$\Pi^1_{\infty}\text{-}\mathsf{CA}_0$ demuestra la existencia de modelos de RTA $_0$ . Pero creo que no implica ATR $_0$ porque el axioma Beta es una especie de axioma de sustitución. ¿Es eso cierto?

Answer 1

Sí, de hecho $\Pi^1_1$ -CA ₀ basta para demostrar ATR ₀ . La forma más sencilla de verlo es que ATR ₀ es equivalente a $\Sigma^1_1$ -separación: si $\phi(n)$ y $\psi(n)$ son $\Sigma^1_1$ fórmulas entonces $$\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)).$$ Suponiendo que $\Pi^1_1$ -CA ₀ uno puede simplemente tomar $C = \lbrace n : \lnot\psi(n)\rbrace$ para satisfacer la conclusión. Encontrará más detalles en Simpson's Subsistemas de aritmética de segundo orden .