Return to Question

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.

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.

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