Skip to main content
1 of 2

All of the traditional "locally predicatively justifiable" theories are supposed to have equivalent $\Pi^1_1$ theorems; but they differ for statements of higher complexity. So they would not, even under the traditional reading, characterize all of second-order predicative arithmetic. Presumably, one would need a predicative version of the Axiom of Projective Determinacy to characterize the provable higher-complexity statements (and of course the analysis would depend on the classical version of this axiom).

But, in fact, something seems to have gone wrong somewhere, because $\mathcal{ATR}_0$ is finitely axiomizable (Feferman points this out on page 21); so it cannot be locally predicatively justifiable. For an explicit example, "For any $\alpha<\Gamma_0$, $RA_\alpha$ is consistent" is a $\Pi_1^0$ sentence provable in $\mathcal{ATR}_0$ but not in $RA_\alpha$ for any $\alpha < \Gamma_0$.