Does iterating the consistency of ZFC answer any natural questions? The following is a natural question that occurred to me, but I'm not sure if it's even well-defined since I haven't read the literature on iterating consistency statements. Let $Con_0(ZFC)=Con(ZFC)$ and, inductively, let $Con_\alpha(ZFC)=Con(ZFC+\{Con_\beta(ZFC): \beta < \alpha\})$. First of all, does this give a well-defined formula in the language of set theory for every ordinal $\alpha$? If not, at what point and for what reason does it go wrong? If it does, since we know that the formal language of set theory only has countably many formulas, we know that this sequence of consistency statements must stop giving new formulas after a certain point. Is it known at what point it starts repeating itself? Also, why isn't the fact that it does repeat itself forever contrary to Godel's Second Incompleteness theorem?
Finally, let us call those statements that we are "committed to" all of those statements that are logical consequences of $ZFC+\{Con_\alpha(ZFC) : \alpha \in ON\}$ (or if this formulation is not well-defined for some reason, up to the highest alpha we can get to). Are there any natural set-theoretic (or non set-theoretic) statements that we are committed to but nonetheless are independent of ZFC? In particular, has anyone shown that we are not committed either way on CH?
 A: This is a famous topic studied by Alan Turing in his dissertation Systems of Logic Based on Ordinals in 1939, and again by Soloman Feferman in 1962.


*

*"Systems of Logic Based on Ordinals", Alan Turing, Proceedings of the London Mathematical Society, s2-45(1), 1939, pp. 161-228. 

*"Transfinite Recursive Progressions of Axiomatic Theories", Solomon Feferman, The Journal of Symbolic Logic 27 (3), 1962, pp. 259-316. Restricted-access URL: http://www.jstor.org/stable/2964649
(Please feel free to edit this post to insert a link to a legitimate, freely available online version of Feferman's paper, if one exists.)
As for where things go wrong, one key issue is that creating a formula for $\text{Con}_\alpha(T)$ requires $\alpha$ to not only be an ordinal, but to be definable by a formula in some way. So the construction goes awry at the first $\alpha$ which is not definable in this way, which will be a countable ordinal due to some results of hyperarithmetical theory. 
For a more modern treatment, you could look at Torkel Franzén, Inexhaustibility: A Non-Exhaustive Treatment, Lecture Notes in Logic v. 16, 2004.  (Link: Review by John Baldwin)
