Metamathematical Properties of $\mathsf{IR}$ and $\mathsf{ATR}_0$

$\mathsf{IR}$ and $\mathsf{ATR}_0$ are similar in the following respects:

1.

They have the same proof-theoretic ordinal: $\vert\mathsf{IR}\vert=\vert\mathsf{ATR}_0\vert=\Gamma_0$.

2.

$\mathsf{IR}$ and $\mathsf{ATR}_0$ prove the same $\Pi^1_1$ sentences.

3.

$\mathsf{IR}$ and $\mathsf{ATR}_0$ have the same proof-theoretic strength.

These results are due to Friedman [10, §4]. The main point that we would like to make here is that $\mathsf{IR}$ and $\mathsf{ATR}_0$ differ greatly in some other, very significant respects. In particular:

1.

$\mathsf{IR}$ explicates predicative provability, while $\mathsf{ATR}_0$ explicates predicative reducibility.

2.

$\mathsf{ATR}_0$ is much stronger than $\mathsf{IR}$, model-theoretically and, above all, mathematically.

The following properties of the two systems indicate how different they are from the metamathematical point of view.

1.

The minimum $\omega$-model of $\mathsf{IR}$ is $\mathrm{HYP}(\Gamma_0)$, i.e., $L_{\Gamma_0}\cap P(\omega)$.

2.

The minimum $\omega$-model of the $\Delta^1_1$ comprehension axiom is HYP, i.e., $L_{\omega_1^{CK}}\cap P(\omega)$.

3.

HYP is the intersection of all $\omega$-models of $\mathsf{ATR}_0$.

4.

$\mathsf{ATR}_0$ has no minimal $\omega$-model.

5.

$\mathsf{ATR}_0$ automatically holds in any $\beta$-model.

6.

HYP is the intersection of all $\beta$-models.

7.

There is no minimal $\beta$-model.

We can also compare $\mathsf{IR}$ and $\mathsf{ATR}_0$ with the perhaps more familiar system $\Pi^1_\infty$- $\mathsf{TI}_0$ consisting of the transfinite induction axiom. The latter system is sometimes known as bar induction. Some metamathematical properties:

1.

$\Pi^1_\infty$- $\mathsf{TI}_0$ includes both $\mathsf{IR}$ and $\mathsf{ATR}_0$. The precise relationship to $\mathsf{ATR}_0$ is that $\Sigma^1_1$- $\mathsf{TI}_0=\mathsf{ATR}_0+\Sigma^1_1$- $\mathsf{IND}$ (Simpson [20]).

2.

$\Pi^1_\infty$- $\mathsf{TI}_0$ is proof-theoretically stronger than $\mathsf{IR}$ and $\mathsf{ATR}_0$.

3.

$\vert\Pi^1_\infty$- $\mathsf{TI}_0\vert=\varphi_{\varepsilon_{\Omega+1}}(0)=$ the Howard ordinal.

4.

$\Pi^1_\infty$- $\mathsf{TI}_0$ has no minimal $\omega$-model.

5.

$\Pi^1_\infty$- $\mathsf{TI}_0$ automatically holds in any $\beta$-model.

6.

HYP is the intersection of all $\beta$-models.

7.

There is no minimal $\beta$-model.

For proofs of the model-theoretic results mentioned above, see chapters VII and VIII of Simpson [24].