Questions of predicativity are well-studied in the context of arithmetic. We have a base theory, first-order Peano arithmetic. Some people, like Edward Nelson (in chapter 1 of his book) and Charles Parsons (in this paper), consider it to be impredicative, because induction allows a formula $\phi$ even if it contains quantifiers which range over the natural numbers, even though natural numbers are conceived as objects which satisfy all inductive formulas, including the formula $\phi$ itself. So Nelson has constructed a subsystem of first-order arithmetic which doesn't allow induction for much more than formulas with bounded quantifiers.
But some people like Weyl and Poincare are willing to accept the natural numbers as given in advance as a completed totality, so they're willing to accept first-order PA, but they're not willing to accept arbitrary sets of natural numbers on a Platonic basis. This leads them to consider second-order PA as impredicative, because its comprehension schema allows a formula $\phi$ even if it contain quantifiers that range over all sets of natural numbers, including the set currently being defined by $\phi$. This leads people to constructing subsystems of second-order PA such as $ACA_0$ whose predicative comprehension schema only allows formulas with no quantification over sets of real numbers.
Yet arithmetic, even though it gets the most focus from predicativist critics, is not the only subject where we run into these issues. They also arise in set theory. Like first-order PA, we have a base theory, ZF (or ZFC if you prefer). Some people consider ZF impredicative, because the seperation schema allows formulas that have quantifiers that range over all sets, including the one being defined. So people have made subsystems of ZF, like Kripke-Platek set theory and Myhill's constructivist set theory, which have a predicative seperation schema which only allows formulas with bounded quantifiers. (This is analogous to Nelson's predicative first-order arithmetic.)
But just like in the case of arithmetic, some people are willing to accept the universe of sets on a Platonic basis, so they accept ZF, but they're not willing to do the same for proper classes. This leads them to reject Morse-Kelley set theory as impredicative, because its class comprehension schema allows quantification over classes, including the one being defined. So just like $ACA_0$, people have constructed a subsystem of MK known as NBG with a predicative class comprehension schema that does not allow quantification over classes.
My question is, has anyone tried to apply the techniques developed to deal with predicativity for arithmetical theories, specifically the ramified theory of types, to predicative set theories? The ramified theory of types is a way to expand the strength of a predicative theory, by breaking an axiom schema into levels. Here is an illustration in the context of second-order arithmetic: we have a comprehension schema for level $0$ sets, which allows no quantification over sets of natural numbers. That's the comprehension schema for $ACA_0$, but we don't stop there. We have a comprehension schema for level $1$ sets, which only allows quantification over level $0$ sets. And in general, for any natural number $n$, the comprehension schema for level $n+1$ sets allows quantification over sets of level $n$ and below. And don't need to stop at finite levels. We can continue to a comprehension schema for level $\omega$ sets which allows quantification over sets of any finite level, and so on, for higher and higher transfinite ordinals.
The ramified theory of types allowed Feferman and Schutte to start from a relatively weak predicative theory $ACA_0$ which was conservative over first-order $PA$, and move to a much stronger predicative theory like $ATR_0$, as I discuss in this question. It similarly allowed Burgess and Hazen to start from Edward Nelson's theory, which was not much stronger than bounded arithmetic, and move to exponential function arithmetic, as I discuss in this question.
So has anyone tried to do similar things to predicative set theories? For instance, we can replace the predicative class comprehension schema of NBG with comprehension schemata for classes of various levels, just like was done for predicative second-order arithmetic. And we can take Kripke-Platek set theory and replace its predicative seperation schema with seperation schemata for sets of various levels. This may allow for the construction of much stronger predicative set theories.
I think this might have some relation to the constructible hierarchy. Can anyone confirm that?
Any help would be greatly appreciated.
Thank You in Advance.
EDIT: I haven't read it, but this chapter from Skolem's book "Abstract Set Theory" may be useful.
