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?

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.

(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)

• Thanks for the references and answer! Do we know the least such ordinal where things go wrong? And do you have any info about the second part of the question - i.e. an example of a natural statement that is independent of ZFC but decided by adjoining however many iterations of consistency are well defined? – David B. Nov 2 '14 at 23:39
• The least ordinal will depend on the theory at hand, but it will be related to the Church-Kleene ordinal $\omega_1^{CK}$ en.wikipedia.org/wiki/Church%E2%80%93Kleene_ordinal . This is a countable ordinal, but large in the sense of this article: en.wikipedia.org/wiki/Large_countable_ordinal . There will not be any nice closed expression for your ordinal. I don't know an answer to the second part offhand. – Carl Mummert Nov 2 '14 at 23:42
• Thanks a lot for the references - I think I'll leave the question open however in hopes for any information on the second part. – David B. Nov 5 '14 at 4:27
• What about $\omega$? It seems that $\mathrm{ZFC}+\{\mathrm{Con}_\alpha(\mathrm{ZFC}):\alpha<\omega\}$ proves its own consistency by the compactness theorem (I mean, if it's inconsistent, then $\mathrm{ZFC}+\{\mathrm{Con}_\alpha(\mathrm{ZFC}):\alpha<n\}$ is inconsistent for some $n$, which contradicts $\mathrm{Con}_n(\mathrm{ZFC})$...). But it can't, because of the second incompleteness theorem... So what am I not seeing? – Cronus Dec 22 '17 at 15:03
• @Cronus: this is one of those questions that everyone works out, then forgets, then has to work out again. Letting $T$ be the theory from the first line of your comment, and letting $T(n) = \text{ZFC} + \{\text{Con}_m(\text{ZFC} : m < n\}$, we are trying to show that $T \vdash \text{Con}(T)$ by contraposition, so we working within $T$ we say: if $\text{Pvbl}_T(0 = 1)$ then, $(\exists r) \text{Pvbl}_{T(r)}(0=1)$ by compactness. However, $T$ does not contain the axiom $(\forall n) \text{Con}_n(\text{ZFC})$, so we do not obtain a contradiction. ... – Carl Mummert Dec 22 '17 at 22:09