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".
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.
My question is, how strong is second-order arithmetic with ramified comprehension? Is it still conservative over first-order PA? How powerful a subsystem of second-order PA is it in the context of reverse mathematics?
Any help would be greatly appreciated.
Thank You in Advance.