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](http://plato.stanford.edu/entries/type-theory/#3), 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.

Thank You in Advance.