Let


ZF1 = ZF,


ZFk+1 = ZF + the assumption that ZF1,...,ZFk are consistent,


ZFω = ZF + the assumption that ZFk is consistent for every positive integer k,


... and similarly define ZFα for every computable ordinal α.


Then a commenter on my blog [asked a question](http://www.scottaaronson.com/blog/?p=663#comment-24470) that boils down to the following: can we give an example of a Π1-sentence (i.e., a universally-quantified sentence about integers) that's provably independent of ZFα for *every* computable ordinal α? (AC and CH don't count, since they're not Π1-sentences.)


An equivalent question is whether, for every positive integer k, there exists a computable ordinal α such that the value of BB(k) (the kth Busy Beaver number) is provable in ZFα.


I apologize if I'm overlooking something obvious.


**Update:** I'm grateful to François Dorais and the other answerers for pointing out the ambiguity in even defining ZFα, as well as the fact that this issue was investigated in Turing's thesis. Emil Jeřábek writes: "Basically, the executive summary is that once you manage to make the question sufficiently formal to make sense, then every true Π1 formula follows from some iterated consistency statement."


So, I now have a followup question: given a positive integer k, can we say something concrete about *which* iterated consistency statements suffice to prove the halting or non-halting of every k-state Turing machine? (For example, would it suffice to use ZFα for *some* encoding of α, where α is the largest computable ordinal that can be defined using a k-state Turing machine?)



Pi1-sentence independent of ZF, ZF+Con(ZF), ZF+Con(ZF)+Con(ZF+Con(ZF)), etc.?
In 1939, Alan Turing investigated such questions [*Systems of logic based on ordinals*, Proc. London Math. Soc. 45, 161-228]. It turns out that one runs into problems rather quickly due to the fact that the $(\omega+1)$-th such theory is not completely well-defined. Indeed, there are many ordinal notations for $\omega+1$ and these can be used to code a lot of information.


**Turing's Completeness Theorem.** If $\phi$ is a true $\Pi\_1$ sentence in the language of arithmetic, then there is an ordinal notation $a$ such that $|a| = \omega+1$ and $T\_a$ proves $\phi$.


This result applies to any *sound* recursively axiomatized extension $T$ of $PA$. In particular, this applies to (the arithmetical part of) $ZF$.


To avoid this, one might carefully choose a path through the ordinal notations, but this leads to a variety of other problems [S. Feferman and C. Spector, *Incompleteness along paths in progressions of theories*, J. Symbolic Logic 27 (1962), 383–390]. 


