As everybody knows, the ZFC axioms may serve as a foundation for (almost)
all of contemporary mathematics, and it is also well-known that several results
are "indecidable" in ZFC, which means that they cannot be proved or disproved within 
ZFC.


It is therefore natural to look for "new axioms" to add to ZFC and make it a
stronger system. But by Godel's second incompleteness theorem, the consistency of
ZFC cannot be deduced from ZFC itself.


Therefore, we may add the axiom "ZFC is consistent" and obtain 
a new system $ ZFC\_1 $ consisting of "ZFC+(ZFC is consistent)". We may
iterate this, and define $ ZFC\_2 $ as "$ZFC\_1$+($ZFC\_1$ is consistent)", etc,
and we may even define $ZFC\_{\omega}$, or $ZFC\_{\alpha}$ for any
ordinal $\alpha$.


This seems a little too easy, so my question to logicians is : is this construction
completely irrelevant to logic ans set theory questions ? If so why? Is it true that the results which are classically independent of ZFC are also
 independent of $ZFC\_1$, $ZFC\_2$, $ZFC\_{\omega}$ etc ?



Using consistency to create new axioms in set theory
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 [blog article](http://xorshammer.com/2009/03/23/what-happens-when-you-iterate-godels-theorem/) 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, provides a more natural environment for the analysis of such 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 T0 = T, T1 = T0 + Con(T0), T2 = T1 + Con(T1), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of Tω or Tω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of [ordinal notations](http://en.wikipedia.org/wiki/Ordinal_notation) 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 these to [subsystems of second-order arithmetic](http://en.wikipedia.org/wiki/Second-order_arithmetic), but there and in set theory the appropriate principles to study are reflection principles and large cardinal axioms which have better semantic interpretations and take advantage of their richer surroundings.


