The first-order theory of real numbers, AKA the theory of real closed fields, is obtained by added to the axioms for ordered fields an axiom schema of completeness, which states that for each formula $\phi$ in the first-order language of ordered fields, if the element satisfying $\phi$ have an upper bound, then they have a least upper bound. The second-order theory of real numbers is obtained by replacing this schema with a single axiom which says that for all sets X, if X has an upper bound then it has a least upper bound. And of course we need a comprehension schema which states that for each formula $\phi$ in the second-order language of ordered fields, there is a set corresponding to $\phi$.
As I found out in response this question, the proof-theoretic ordinal of the theory of real closed fields seems to just be $\omega$. But what about the proof-theoretical ordinal of the predicative second-order theory of real numbers? This theory is obtained by taking the ordinary second-order theory of real numbers, but restricting the comprehension schema to formulas with no second-order quantification. Would this theory have a proof-theoretic ordinal greater than $\omega$?
The reason I ask is my MathOverflow question, which is about the possibility of a Feferman-Schutte-like analysis of "predicativity given the real numbers".
Any help would be greatly appreciated.
Thank You in Advance.
