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 emphasize why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The problem 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.) Analyzing such arithmetical statements in ZFC is overkill, PA is a much more appropriate theory for doing this, but there is an even more fundamental problem.

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.