MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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 '12 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 '12 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 '12 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 '12 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 '12 at 17:42
up vote 6 down vote accepted

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.

share|cite|improve this answer
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 '12 at 15:22

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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