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". 

Impredicativity manifests itself in second-order theories by having a comprehension schema that allows formulas that have bound set variables in them, where the set variables can range over the set being defined.  In the case of second-order arithmetic, the standard way to ensure predicativity is the ramified theory of types, which breaks up the comprehension schema into levels: we have a comprehension schema for level $0$ sets that doesn't allow any bound set variables.  This gives us a theory known as $ACA_0$, and it is conservative over first-order $PA$.  And then for any $n$, we have a comprehension schema for level $n + 1$ sets that only allows quantification over sets of level $n$ and below.  And there's no reason to stop at finite levels: we can define a schema for set $\omega$ sets, for instance, which allows quantification of any sets of finite level, and we can go to even bigger transfinite ordinals.  Feferman and Schutte reached the conclusion that if you only allow a schema for level $\alpha$ sets if it's predicatively provable (using comprehension schemata for lower levels) that $\alpha$ exists (i.e. there's a well-ordering of the natural numbers with order-type $\alpha$), then predicativity will allow you a comprehension schema for all levels $\alpha$ less than a certain ordinal $\Gamma_0$, the Feferman-Schutte ordinal.  See my question [here][1] for more details.

The Feferman-Schutte analysis represents an attempt to define the notion of "predicativity given the natural numbers".  In other words, if we accept the set of natural numbers as a completed totality, but we don't accept arbitrary subsets of the set of natural numbers, we're trying to find what sets of natural numbers we can accept on a predicative basis.  My question is, can we do the same thing with the notion of "predicativity given the real numbers", i.e. accepting the set of real numbers as a completed totality, but not arbitrary subsets of the set of real numbers, what sets can we accept on a predicative basis?

We can start in the same manner as second-order arithmetic: we can have the axioms for ordered field, the least upper bound axiom (AKA Dedekind-completeness), and a comprehension schema for level 0 sets allowing no bound set variables.  This would yield an analogue of $ACA_0$, i.e. a system that is conservative over the first-order theory of real closed fields.  And we can define a schema for each finite level the same way as before.  But how do we proceed after that?  Are we allowed to iterate to transfinite ordinals, and if so which transfinite ordinals are we allowed to iterate to?  What countable well-orderings can be defined using the second-order theory of real numbers, especially with a predicativity restriction?  Would defining $\omega$ requiring recognizing the set of natural numbers, and how can we do that, if the standard way to define "natural number" is in terms of the impredicative definition of "inductive number" given at the top of the post?  

What is the proof-theoretic ordinal of the first-order theory of real closed fields? And whatever it is, are we allowed to iterate up to it, just as Feferman and Schutte started by iterating the comprehension schema up to level $\epsilon_0$, the proof theoretic-ordinal of first-order $PA$?

Any help would be greatly appreciated. 

Thank You in Advance.

EDIT: As discussed in [my Math.SE thread][2], the first-order theory of real closed field cannot prove the well-foundedness of any transfinite ordinals, because the only sets it can define are semialgebraic sets, which are finite unions of points and intervals, so it can't define any countable ordinals.  So I guess the proof-theoretic ordinal of the first-order theory of real closed fields would just be $\omega$, which doesn't help us.  But what if took the analogue of $ACA_0$, i.e. the axioms for ordered fields along with the least upper bound axiom (AKA Dedekind completness), but with comprehension restricted to formulas with no quantification over sets?  Would that theory be able to define any countable well-orderings?  If its proof-theoretic ordinal was greater than $\omega$, then we can use it to define comprehension schemata with transfinite levels, so we could carry out a Feferman-Schutte-like analysis. 


  [1]: http://mathoverflow.net/questions/143225/does-the-feferman-schutte-analysis-give-a-precise-characterization-of-predicativ
  [2]: http://math.stackexchange.com/questions/512584/what-is-the-proof-theoretic-ordinal-of-the-first-order-theory-of-real-closed-fie