Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book *Inexhaustibility: a non-exhaustive treatment* (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent <a href="http://xorshammer.com/2009/03/23/what-happens-when-you-iterate-godels-theorem/">blog article</a> by Mike O'Connor.

----------

Note: The following is explained in Mike O'Connor's article, but I think I need to clarify why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The idea is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) This is why PA, or more generally any recursively axiomatizable extension of PA, which provide a more natural environment for the analysis of arithmetical statements. For example, instead of ZFC, you may as well use the purely arithmetical part of ZFC.

There is also an even more fundamental problem with transfinite iterates. Given a recursive presentation of a theory T, the iterates T<sub>0</sub> = T, T<sub>1</sub> = T<sub>0</sub> + Con(T<sub>0</sub>), T<sub>2</sub> = T<sub>1</sub> + Con(T<sub>1</sub>), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of T<sub>&omega;</sub> or T<sub>&omega;+&omega;+3</sub> but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of <a href="http://en.wikipedia.org/wiki/Ordinal_notation">ordinal notations</a> than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.

These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend to <a href="http://en.wikipedia.org/wiki/Second-order_arithmetic">subsystems of second-order arithmetic</a>, but there and, more generally, in set theory the appropriate principles to study are reflection principles and large cardinal axioms which have better semantic interpretations.