2

$\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?

flag
I'm puzzled with your reference to Axiom Beta since that is not part of $\mathsf{ATR}_0$. It's true that it is part of Simpson's $\mathsf{ATR}_0^{\mathsf{set}}$ but that is a little accidental. Is that what you're talking about? – François G. Dorais♦ Dec 4 at 3:52
You can prove an independence claim in the arithmetic by citing one in set theory. I do not understand what you mean is accidental. $\mathsf{ATR}_0$ and $\mathsf{ATR}_0^{\mathrm{set}}$ are bi-interpretable by design. – Colin McLarty Dec 4 at 15:47
You have to be very careful when mixing interpretation and provability. For example, ZFC (which includes foundation) is biinterpretable with Aczel's AFA (which refutes foundation). What I mean by "accidental" is that Axiom Beta is a byproduct of the interpretation and not an essential part of it. – François G. Dorais♦ Dec 4 at 16:31
Yes, but you can draw conclusions more quickly when one side of the bi-interpretation is a conservative extension, as $\mathsf{ATR}_0^{\mathrm{set}}$ is a conservative extension of $\mathsf{ATR}_0$. Axiom Beta posits precisely that certain transfinite recursions can be done in set theory, corresponding by design to arithmetic transfinite recursion as a subsystem of $Z_2$. – Colin McLarty Dec 4 at 16:56
That's another subtle trap: $\mathsf{ATR}_0^{\mathsf{set}}$ is a conservative extension of $\mathsf{ATR}_0$ only in the loose sense since the language of second-order arithmetic is technically not a subset of the language of set-theory. In this case, the trap is not so bad since there is a canonical translation of the language of second-order arithmetic into the language of set theory. However, Axiom Beta falls right into this trap since it cannot be formulated (in a non-trivial way) in the language of second-order arithmetic. – François G. Dorais♦ Dec 4 at 17:42
show 1 more comment

1 Answer

6

Yes, in fact $\Pi^1_1$-CA0 suffices to prove ATR0. The simplest way to see this is that ATR0 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$-CA0 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.

link|flag
It is p. 271, with a concise proof. I think my systematic error was not keeping in mind that hereditary countability includes existence of transitive closures, and so proves a lot of things usually proved by replacement. – Colin McLarty Dec 4 at 15:22

Your Answer

Get an OpenID
or

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