Did Gödel prove that the Ramified Theory of Types collapses at $\omega_1$?

Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set being defined. The standard resolution to this impredicativity is known as the Ramified Theory of Types, which divides the comprehension schema into levels. The comprehension schema for level $0$ sets does not allow formulas with any second-order quantification. The schema for level $1$ sets only allows quantification over level $0$ sets. For any natural number n, the schema for level $n+1$ sets allows quantification over sets of level $n$ and below.

But there's no obvious reason why we need to stop at finite levels. For instance, the schema for level $\omega$ sets allows quantification over sets of all finite levels. And so on, for higher and higher transfinite ordinals. The question is which ordinals to use. One viewpoint is that we should be predicative about our choice of ordinals as well. This means that we should only allow a comprehension schema for level $\alpha$ sets if we have already shown using lower-level comprehension schemata that $\alpha$ is a well-founded ordinal. Feferman and Schütte showed that if we proceed in this manner, then we'll ultimately get levels corresponding all ordinals up to a certain ordinal known as $\Gamma_0$, the Feferman-Schütte ordinal.

But it seems that before Feferman and Schütte, Gödel pursued an alternate approach in which we adopt a Platonistic as opposed to a predicativist view concerning what ordinals to use to index our comprehension schemes. And according to this Stanford Encylopedia of Philosophy article, he was apparently able to show that if you kept going to higher and higher ordinals, the Ramified hierarchy "collapses" at the ordinal $\omega_1$ (the least uncountable ordinal), in the sense that if you went to higher levels than that you can't prove any more statements.

First of all, is it true that Gödel proved such a result? If so, why is it that start with an arithmetical theory $T$ and keep adding consistency principles like $Con(T)$ and $Con(T+Con(T))$ and so on, this procedure collapses at the ordinal $\omega_1^{CK}$ (the least non-recursive ordinal), yet here you have to go all the way up to $\omega_1$?

More importantly, if you do make the levels go up to $\omega_1$, how much arithmetic can you prove in the resultant theory? Can you prove as much as second-order arithmetic can? Or can you only prove as much as some weaker subsystem of second-order arithmetic, and if so, how does that subsystem fit into the framework of reverse mathematics? What is the proof-theoretic ordinal of this theory?

Any help would be greatly appreciated.

-

I believe that the result you ask about follows from Gödel's theorem that no new sets of natural numbers occur after stage $\omega_1$ of the constructible hierarchy of sets. That hierarchy, like the ramified hierarchy you describe, forms, at each stage, only those sets that are (parametrically) definable over what was produced at earlier stages. It differs from yours in that it constructs not only sets of natural numbers but also sets of those, and sets of sets of those, etc. It seems to me that, by considering the two hierarchies together, one can show that every set that occurs in the ramified hierarchy also occurs at the same level or sooner in the constructible hierarchy. (This needs some checking, which I think amounts to simulating the ramified hierarchy, stage by stage, in the constructible hierarchy. The simulation must be done carefully, because the constructible hierarchy will, I believe, produce some sets of natural numbers earlier than the ramified hierarchy does, so the ramified hierarchy is not simply the restriction of the constructible one to sets of natural numbers.)

Instead of comparing with the constructible hierarchy, one could, I believe, obtain a stronger result by a Löwenheim-Skolem argument, namely it should be provable that the ramified hierarchy stops strictly earlier than $\omega_1$.

Going out on a limb, I'll venture the opinion that the ramified hierarchy ends at the first ordinal $\alpha$ at which the constructible hierarchy produces no new sets of natural numbers. It is known (by another Löwenheim-Skolem argument) that this $\alpha$ is countable. I'm quite confident that the end of the ramified hierarchy is $\leq\alpha$, but I'm not so sure about the reverse inequality. (I believe the end of the ramified hierarchy is also known as "the ordinal of the least $\beta$-model of analysis".)

-
Do you have any idea about how much arithmetic we can prove if we go up to $\omega_1$? Like what subsystem of second-order arithmetic does it correspond to? –  Keshav Srinivasan Dec 8 '13 at 2:22
@KeshavSrinivasan I think that the model you get this way will satisfy full second-order arithmetic, in the sense of having the full comprehension axiom ($\Pi^1_\infty$-comprehension). If that failed, you'd get more sets of natural numbers at the next step of the hierarchy. I would also expect that this model admits a definable well-ordering, similarly to what happens in the constructible universe. –  Andreas Blass Dec 9 '13 at 0:09
How would you prove that you'd get more sets of natural numbers at the next level if you didn't get full second-order comprehension at the current level? That would surprise me, since I would have thought there are some theorems of second-order arithmetic that are simply impredicative, and could never be reached by the ramified hierarchy. –  Keshav Srinivasan Dec 9 '13 at 5:30
With your meaning of "full comprehension", I don't see any chance for connecting it to the ramified hierarchy in general. My meaning, on the other hand, corresponds to saying that the structure satisfies the axiom schema of second-order comprehension, which seems close to what you asked in your first comment (about "system[s] of second-order arithmetic"). –  Andreas Blass Dec 12 '13 at 19:59
@KeshavSrinivasan Now I really don't understand you. One of your comments says you weren't talking about interpreting the quantifiers at all. In an earlier comment you wrote "even if it has quantification over ALL sets". These two look contradictory to me. The usual interpretation of second-order quantifiers in a model of (all or part of) second-order arithmetic is that they range over the sets in that model. Quantification over ALL sets (even those not in the model) is a very different interpretation of quantification. –  Andreas Blass Dec 13 '13 at 17:43

I was reading Feferman's original 1964 paper "Systems of Predicative Analysis", and I think I've found an answer to my question about how much second-order arithmetic you can do if you let the ramified hierarchy go high enough. Feferman defines $M_\alpha$ to be the collection of all sets defined by comprehension schemes for level $\alpha$ and below. And on page 10 of the paper, Feferman says that Kleene proved in this paper that "$M_{\omega_1}$ consists exactly of the hyperarithmetic sets." Now one concern I have is that Feferman seems to be using the notation $\omega_1$ to refer to the Church-Kleene ordinal $\omega_1^{CK}$ rather than the first uncountable ordinal, which he denotes by $\Omega$.

But the work that Feferman does on page 11 somewhat alleviates this concern. For any collection of sets $D$, a formula $\phi$ is said to be "definite relative to $D$" if $\phi(x)$ if and only if $\phi_D(x)$, where $\phi_D$ is the formula obtained by restricting all the second-order quantifiers in $\phi$ to the sets in $D$. Let us define $D_0$ to be the collection of all sets defined by formulas with no second-order quantifiers. For any natural number $n$, let $D_{n+1}$ consist of all the sets in $D_n$ together with all the sets defined by formulas which are definite relative to $D_n$. And then $D_\omega$ is equal to the union of $D_n$ for all $n$. And so on, for higher and higher ordinals. Now Feferman shows that $D_{\Omega+1} = D_\Omega = D_{\omega_1}$, all of which are equal to the collection of hyperarithmetic sets.

Now Feferman doesn't explicitly say this, but I assume that analogously, $M_\Omega = M_{\omega_1}$. Can anyone back me up on that? If I'm right about that, and if the Stanford Encylopedia of Philosophy article is right that the ramified hierarchy collapses at $\Omega$, then that would mean that letting the ramified hierarchy go arbitrarily high would only get you to the hyperarithmetic sets, which is considerably weaker than what full second-order comprehension buys you.

-