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 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, 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.
EDIT 2: It occurs to me that since $RCF$ is complete, any consistent extension of $RCF$ is trivially conservative over $RCF$. Thus we can't mimic the proof that $ACA_0$ has ordinal $\epsilon_0$, which goes roughly as follows: if $ACA_0$ could prove the well-foundedness of all ordinals less than $\alpha$ for some $\alpha > \epsilon_0$, then it could prove some statements of arithmetic that $PA$ cannot prove, which is impossible since $ACA_0$ is conservative over $PA$. But this wouldn't work in our case, because $RCF$ + "the ordinals up to $\alpha$" is always conservative over $RCF$.
So the question still remains, how can you determine what countable well-orderings are definable in the second-order theory of real numbers, with comprehension restricted to formulas with no second-order quantification?
EDIT 3: I think that the full second-order theory of real numbers can be interpreted in third-order Peano arithmetic. So is it possible that the predicative second-order theory of real numbers bears some relation to predicative third-order arithmetic?
EDIT 4: Some recent work by Feferman may have some bearing on this question; see his paper, the slides for his accompanying talk, and the video of the talk. Feferman consider the question of what would happen if we take a Platonistic view toward the set of all natural numbers $N$ AND the powerset of the set of natural numbers $P(N)$, but we do not adopt a Platonistic view toward the powerset of that set, $P(P(N))$. Now the set of real numbers is isomorphic to $P(N)$, so another way of saying this is that we view natural numbers and real numbers on a Platonistic basis, i.e. as a completed totality, but we develop sets of real numbers predicatively. On this basis, he constructs an extension of Kripke-Platek set theory in which classical logic applies to statements with bounded quantifiers, but intuitionistic logic applies to statements with unbounded quantifiers. I don't know whether this extension takes advantage of the ramified theory of types and autonomous progressions that are the hallmark of the Feferman-Schutte analysis. In any case, under this system there are some statements with unbounded quantifiers which we can prove that the law of excluded middle applies to. Feferman conjectures that the Continuum Hypothesis is not one of them, so he concludes that the Continuum Hypothesis does not have a meaningful truth value if you only adopt a Platonistic attitude toward $N$ and $R$ but not $P(R)$
Keep in mind that my question asks something slightly different: it's about what happens if you only adopt a Platonistic attitude toward $R$, not a platonistic attitude toward $N$ or $P(R)$. But is there a connection between Feferman's work and my question?
At least it places an upper bound on what can be proved with the notion of "predicativity given the real numbers". The proof-theoretic ordinal of Kripke-Platek set theory is the Bachmann-Howard ordinal, which is greater than the Feferman-Schutte ordinal, and I assume that Feferman's extension of Kripke-Platek set theory has an even higher proof-theoretic ordinal. So it seems that "predicativity given the natural numbers and real numbers" yields more ordinals than predicativity given the natural numbers alone. So does that mean that predicativity given the real numbers alone yields some nontrivial ordinals?
EDIT 5: I emailed Solomon Feferman, and he suggested that applying his unfolding program, which he previously applied to Peano Arithmetic here and "finitist arithmetic" here, to the first-order theory of real closed fields may be the way to formalize the notion I'm talking about. (Unfolding is a procedure that's applied to axiom schemata, so we would apply it to the least upper bound axiom schema of the first-order theory of real closed fields.) Does anyone familiar with the unfolding program know how I would go about doing this?
[Also, a semantic note: If we are considering theory of real closed fields as fundamental, then should we say "predicativity given the algebraic real numbers" or "predicativity given the first-order definable real numbers" rather than just "predicativity given the real numbers"? After all, shouldn't predicativity given the real numbers imply predicativity given the natural numbers, since natural numbers are real numbers? But maybe being "given" the natural numbers Platonically is different from being able to "pick them out from a crowd".]