MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top


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

share|cite|improve this question
up vote 16 down vote accepted

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].

share|cite|improve this answer
Wow, thanks François! I didn't know about the connection to Turing's thesis. But how do we reconcile your answer with Joel's very different answer? – Scott Aaronson Jun 8 '11 at 11:21
Torkel Franzen's book Inexhaustibility gives a nice accessible account of the issues involved in trying to pile on consistency statements. As François says, the first thing to wrap your mind around is that "similarly defining $ZF_\alpha$ for every computable ordinal $\alpha$" is a far more subtle task than it might seem at first glance, as you'll quickly discover if you try to write down a careful, rigorous definition yourself. – Timothy Chow Jun 8 '11 at 14:25
Thanks, I just ordered Inexhaustability! – Scott Aaronson Jun 8 '11 at 15:00

I think there is some vagueness inherent in the "similarly define ...". How is one to assign the consistency statement $Con(ZF_\lambda)$ for computable $\lambda$? This looks trivial but it is not.

I think also ZF is something of a red herring here. The question arises in PA (since we are looking at $\Pi_1$ sentences quantifying over natural numbers.)

Feferman has shown ("Transfinite Recursive Progression of Theories" JSL 1962) that it is possible to assign for every n in an effective manner a $\Sigma_1$-formula $\varphi_n(v_0)$ where each of the latter is to be thought of as enumerating (integer codes of) axiom sets (which I'll call "theories."). This is done in such a fashion so that if $a,b$ are integers with $b = 2^a$ that $T_b$ is $T_a$ together with the statement

$$\forall \psi \in \Sigma_1\forall x [ Prov_{T_a}\psi(x) \longrightarrow \psi(x)]$$

(This is thus a "1-Reflection Principle" - for $\psi\in\Sigma_1$ here). He does this with a view to considering those integers $a$ that are notations for recursive ordinals (in the sense of the notation system devised by Kleene - "Kleene's $O$".)
(There are clauses for $a$ representing a notation for a limit ordinal, when $a = 3^e$).

He proves that there are linear paths through the system of notations of computable ordinals, going through all recursive ordinals $\alpha$,so that

Every true $\Pi_2$ sentence in arithmetic is proven by one of the theories along the path.

The starting theory $T_0$ here can be PA (or ZFC if you want). Such a path gives a definite meaning to $ZF_0, \ldots, ZF_\alpha, \ldots$ etc. for recursive $\alpha$.

Moreover for such a particular progression of theories one would would construe the answer to the question to be "No".

Feferman's starting point was the 1939 paper of Turing ("On Systems of Logic Based on Ordinal"). Turing also considered such paths through Kleene's $O$, but could just prove a theorem for $\Pi_1$ sentences, (using simpler "Consistency" statements"). Feferman shows that if one takes "$n$-Reflection" statements for every $n$ each time one extends the theory then there are paths along which every true statement of arithmetic is proven.

The moral of the story is that there are very complex ways of simply defining sequences of theories, (because there are infinitely many ways, or Turing programs, of representing a recursive ordinal) which can hide/disguise all sorts of information.

A very readable survey is Franzen: "On Transfinite Progressions" BSL 2004.

Update (This is an answer to Scott Aaronson's Update.)

He asks: 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?

Let $M_0, \ldots ,M_{n-1}$ enumerate the $k$-state TM's. Let $P$ be the subset of $n$ of those indices of TM's in the list that halt.

The statement

$\forall i (i \in P \rightarrow M_i$ halts $ \wedge \, i \notin P \rightarrow M_i $ does not halt $)$

is a $\Pi_2$ statement. In Feferman's paper (op.cit.) he shows that every true $\Pi_2$ statement is proven by a theory $T_a$ in a 1-Reflection sequence, where $a$ is a notation for an ordinal of rank equal to $\omega^2 + \omega + 1 $.

So in terms of the question we do not need to vary the $\alpha$ depending on what ordinals a $k$-state machine can produce. (Just fix $\alpha$ as given above.) Of course it gives us zero practical information: there are infinitely many such notations of that rank, and we may not know which one to look at.

share|cite|improve this answer
The $\Pi^0_2$ statement in the update is a tautology, it follows from the law of excluded middle. – Emil Jeřábek Jun 9 '11 at 14:46
Thank you Emil, it was indeed idiotic! Amended version follows. – Philip Welch Jun 11 '11 at 18:41
By the way, since $P$ is fixed and finite, the $\forall i(i\in P\to\dots$ part is $\Sigma^0_1$ and accordingly provable already in $Q$, so you can ignore it, and the remaining $\forall i(i\notin P\to\dots$ part is only $\Pi^0_1$. – Emil Jeřábek Jun 11 '11 at 19:06
Emil: Thanks again, yes, good point, so Turing and rank $\omega +1$ suffices? – Philip Welch Jun 12 '11 at 6:42
I think so. – Emil Jeřábek Jun 12 '11 at 10:53

This should be a comment since I don't know the answer, but you might like this article:

It discusses $PA_\alpha$ for ordinal $\alpha$ and mentions things get messy above $\alpha=\omega$.

share|cite|improve this answer

Update. This answer is incorrect for the reasons mentioned in the comments below and the other answers. But I'll leave it up, since it nevertheless does provide natural examples of $\Pi_1$ statements that are independent of some of the naturally formulated $ZFC_\alpha$ for quite a long way. But as the others have mentioned, complications arise in finding such natural denotations of ordinals as one progresses and in the assumption that such denotations are well-founded.

The essence of my argument below is the observation that if there is an transitive model of ZFC or even just an $\omega$-model of ZFC, then from the truth of an arithmetic statement $\phi$, we may deduce that $\phi$ is also true inside the $\omega$-model (because it has the same arithmetic that we do), and hence $Con(ZFC+\phi)$ is true. By iterating this observation, one deduces $ZFC_\alpha$ for any $\alpha$ for which the induction can be carried out.

You didn't say in which theory you wanted the independence proof to exist, but since this background theory must in particular imply the consistency of each theory $ZFC_\alpha$, it is natural to work in a large cardinal background theory. In this case, you can make such statements using large cardinal consistency statements.

For example, the consistency statement Con(ZFC + there is an inaccessible cardinal) is $\Pi_1$, as is any consistency statement of a computably axiomatizable theory, and if it is true, as commonly believed, then it is not provable in any of your theories $ZFC_\alpha$, since the existence of an inaccessible cardinal implies the existence of a transitive model of ZFC, which implies all the theories $ZFC_\alpha$. But meanwhile, this assertion is a very mild large cardinal assumption, that almost all set theorists believe is consistent, and much stronger consistency statements are routinely used in set theory.

In particular, from a stronger large cardinal hypothesis, we can prove that the given consistency statement is a $\Pi_1$ statement independent of each $ZFC_\alpha$, as you desire.

More generally, most all assertions of the form Con(ZFC + there is a large cardinal of a certain type) will be $\Pi_1$ statements that are independent of your theories $ZFC_\alpha$, provably so from a stronger large cardinal assumption.

The large cardinals are quite natural here, since your theories $ZFC_\alpha$ can be viewed as climbing the very bottom initial stages of the large cardinal hierarchy, since they have increasing consistency strength, and one of the principle unifying ideas of the large cardinal hierarchy is that it provides a measure of such consistency strengths. Any "provably" independent statement will need at the very least to prove the consistency of the $ZFC_\alpha$ theories themselves, and therefore must reach nontrivially into this consistency strength hierarchy.

Finally, here is another example provable in a somewhat weaker background theory. Consider the statement asserting that it is consistent with ZFC that there is a transitive model of ZFC. This assertion is routinely made as a simplying assumption in set-theoretic arguments involving forcing, although forcing can be done without it, and being a consistency statement, it is $\Pi_1$. But if there is a transitive model of ZFC, then it is easy to see by induction that each $ZFC_\alpha$ is consistent. Indeed, even an $\omega$-model of ZFC suffices, since any $\omega$-model of ZFC has the same proofs and the same consistency statements being true as in the ambient background with that $\omega$. Thus, the consistency of a transitive model of ZFC or of an $\omega$-model of ZFC implies the consistency of ZFC and of Con(ZFC) etc., of every $ZFC_\alpha$.

share|cite|improve this answer
Thanks, Joel! I actually guessed that the Pi1-sentence I was looking for would likely have the form Con(ZFC+LC), for some large-cardinal axiom LC. But I didn't know the concept of a "transitive model" of ZFC, by which one can prove that such a statement is indeed independent of ZFC_alpha for every alpha. – Scott Aaronson Jun 8 '11 at 11:08
An obvious followup question would be: does there exist a Pi1-sentence that's independent of ZFC+LC, for EVERY large-cardinal axiom LC? But I suppose we're going to run into trouble when we ask in which background theory we'd like that independence to be proven? (And maybe also run into trouble in formalizing what we mean by a "large-cardinal axiom"?) – Scott Aaronson Jun 8 '11 at 11:13
This is all wrong. ZFC + inaccessible cardinal does not prove the consistency of every $ZFC_\alpha$. The reason is that it is a resursively axiomatized theory, and therefore there exists a computable ordinal $\alpha$ which is not provably well-ordered in ZFC (or ZFC + inaccessibles). François Dorais is on the spot below. Basically, the executive summary is that once you manage to make the question sufficiently formal to make sense, then every true $\Pi^0_1$ formula follows from some iterated consistency statement. – Emil Jeřábek Jun 8 '11 at 11:24
Yes, Emil is right...I retract my answer. – Joel David Hamkins Jun 8 '11 at 12:26
Thanks again, Joel! – Scott Aaronson Jun 8 '11 at 12:34

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.