A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies to $n + 1$ whenever it applies to $n$, and you define an inductive number to be any number that has all the hereditary properties of $0$, then the definition of "inductive" involves quantification over all hereditary properties, including the property "inductive". If you're sufficiently Platonistic concerning sets of natural numbers, that won't concern you, because you can say for instance that $0$ obviously has ALL the properties of $0$, so in particular it has all the hereditary properties of $0$, so it's inductive. But predicativists like Weyl and Poincare would say that in order to verify that $0$ is inductive, we need to know what hereditary properties it has, and in order to know what hereditary properties it has, we need to verify that it has the hereditary property known as inductiveness!
In the context of second-order logic, impredicative comprehension refers to any instance of the second-order comprehension schema that involves bound set variables. If we take second-order arithmetic and allow only predicative comprehension, i.e. we only apply the comprehension schema to formulas with no bound set variables, then we get a subsystem of second-order $PA$ known as $ACA_0$, which is conservative over first-order $PA$. But disallowing bound set variables is not the only way to ensure predicativity. We can instead adopt the ramified theory of types, which breaks the comprehension schema into levels. The comprehension schema for level $0$ sets allows no bound set variables. The schema for level $1$ sets allows quantification over level $0$ sets. In general, the schema for level $n + 1$ sets allow for quantification over sets of level $n$ and below. This way, you can still quantify over sets, but you won't risk quantifying over the set you happen to be defining.
And there's no particular reason to stop at finite levels. We can define a comprehension schema for level $\omega$ sets, for instance, allowing quantifies to range over sets of finite level. And so on, going to bigger and bigger transfinite ordinals. Godel apparently showed that if you carried this process all the way up to $\omega_1$, the first uncountable ordinal, you wouldn't need to go any further. But this is somewhat problematic, since there are presumably countable ordinals whose existence aren't even provable by predicative means. In other words, for sufficiently great ordinals $\alpha$, it may not be predicatively provable that there exists a well-ordering of the natural numbers with order-type $\alpha$. Feferman and Schutte remedied this by only allowing a comprehension-schema for level $\alpha$ sets if the ordinal $\alpha$ is in fact predicatively acceptable (using the comprehension-schemata for lower-level sets). See pg 15-16 of this paper for a brief explanation. In any case, they reached the following conclusion: if $RA_\alpha$ denotes second-order arithmetic with a comprehension schemata for sets of level $\alpha$ and below, then $RA_\alpha$ is only predicatively acceptable if $\alpha$ is less than a certain ordinal known as $\Gamma_0$, the Feferman-Schutte ordinal.
My question is, assuming the Feferman-Schutte analysis of predicativity is accurate, can we give a precise criterion for what is and isn't provable in predicative second-order arithmetic. That is, given a sentence $S$ in the language of second-order arithmetic, under what conditions does there exist an $\alpha < \Gamma_0$ such that $S$ is provable in $RA_\alpha$? Of course, such a characterization of what truths are predicatively acceptable would not itself be predicatively acceptable. It's similar to how the truths provable in Edward Nelson's system of predicative first-order provable are precisely the bounded consequences of $Q$ + bounded induction + "exponentiation is total", even though Nelson himself would reject that characterization because he doesn't think exponentiation IS total.
It seems to me that just like $Q$ + bounded induction + "exponentiation is total" is an "upper bound" for Nelson's predicative first-order arithmetic, the system $ATR_0$, Arithmetical Transfinite Recursion, is an "upper bound" for the Feferman-Schutte conception of predicative-second order arithmetic. After all, the proof-theoretic ordinal of $ATR_0$ is $\Gamma_0$, the least impredicative ordinal, and it proves the consistency of $ACA_0$, a predicative subsystem of arithmetic. So can we characterize the set of predicatively acceptable theorems as some appropriate subset of the set of theorems of $ATR_0$, distinguished by some syntactic property, just like we could take the bounded consequences of $Q$ + bounded induction + "exponentiation is total"?
Any help would be greatly appreciated.
Thank You in Advance.
EDIT: As @AndreasBlass pointed out, on page 18 this paper, Feferman says that $ATR_0$ is "locally predicatively justifiable", meaning that a predicativist would reject the system as a whole as impredicative, but would accept each individual theorem of the system as predicatively acceptable, i.e. each theorem of $ATR_0$ is provable in $RA_\alpha$ for some $\alpha < \Gamma_0$ (where $\alpha$ can vary). So now the question becomes, is $ATR_0$ "maximally locally predicatively justifiable"? In other words, are there predicatively acceptable statements of second-order arithmetic not provable in $ATR_0$? And if so, is there some larger system that IS maximal? I assume any such system would still have proof-theoretic ordinal $\Gamma_0$. (Am I right about that?)
