What is the depth of the “provability heirarchy”?

I am not a logician or set theorist, so hopefully this makes sense. Let $T$ be a theory which is expressive enough to make statements like "Statement $A$ has a proof in $T$"; for example, $T$ might be capable of expressing elementary arithmetic and proving certain basic arithmetic facts.

Let $\Pi^0(T)$ consist of those statements $A$ in $T$ such that either $A$ or $\neg A$ admits a proof in $T$. In general, for $i\in \mathbb{N}$ let $\Pi^i(T)$ consist of those statements $A$ such that the statement "Con(T) implies that there does not exist a proof of $A$, or a proof of $\neg A$, in $T$" is in $\Pi^{i-1}(T)$. Intuitively, $\Pi^1$ should consist of those statements $A$ for which one can prove in $T$ that neither $A$ nor $\neg A$ admits a proof in $T$, $\Pi^2$ should consist of those statements $A$ such that one can prove in $T$ that one cannot tell whether or not they admit a proof, but where one knows this fact, and so on.

Godel's first incompleteness theorem implies that $\Pi^0(T)$ does not contain every sentence of $T$; in particular, the proof amounts to constructing a sentence in $\Pi^1(T)$.

Now I'm sure that if this heirarchy is not nonsense for some reason that I'm missing, then it must be well-studied. So here goes:

1) If this set-up is studied, what is it called?

2) In standard theories, e.g. ZFC, is every sentence contained in $\bigcup_{i\in \mathbb{N}} \Pi^i(T)$? It seems to me that any ZFC proof that this is not the case must be non-constructive, and so would be pretty interesting.

3) Are there any standard theories $T$ of finite (known) depth in this heirarchy, i.e. every sentence is contained in $\Pi^i(T)$ for some fixed $i>0$? If so, can this be proven in $T$?

4) One can also define this heirarchy in a relative setting; e.g. one can take two theories $T\subset S$ and ask about $S$-proofs of statements about the existence of proofs in $T$. Is this studied? Are answers to the above questions known in these cases?

Motivation: I recently watched this talk by Voevodsky, and ever since I've been wondering about how much we actually know about what we can prove. One might hope that even if we can't prove every "true" statement, then we can at least always prove that a statement does not admit a proof in our theory, if that is indeed the case. That seems unlikely, and amounts to the claim that all statements in our theory are in $\Pi^1(T)$, but I think that it is the best situation one can hope for (at least naively) given Godel's theorems. So, is the situation hopeless? Give it to me straight, doc.

-
First, note that the usual theories (like PA or ZFC) don't literally say "Statement $A$ has a proof in $T$"; what they actually do is code such statements in some way such that, in the standard model, these codes correspond in some well-understood way to actual proofs. Usually this is a minor point, but I bring it up because when you talk about a $\Pi^\alpha(T)$ hierarchy for arbitrary ordinals $\alpha$, this coding suddenly becomes problematic. As soon as $\alpha$ is infinite, you have to start worrying about how you're going to express $\Pi^\alpha(T)$ inside the theory $T$. –  Henry Towsner Oct 29 '10 at 22:50
I eliminated the ordinal claim, altered the definitions in response to your comment. Hopefully this works now? I do think the ordinal encoding does work for the relative situation I describe in (4), however. –  Daniel Litt Oct 30 '10 at 0:03
add comment

2 Answers

I believe the concept you are looking for is that of "iterated consistency extension." A very nice treatment is given by Torkel Franzén in his book Inexhaustibility: a non-exhaustive treatment. See also this related question and this blog article by Mike O'Connor.

-
Thanks! Since it took me a second to realize the connection between these two notions, I'll spell it out here. The consistency extension of the theory $T$ is "$T$+Con($T$)"; so $\Pi^0("$T$+Con($T$)")=\Pi^1(T)$ and so on. So $\Pi^i(T)$ are exactly the set of statements $A$ such that $A$ or $\neg A$ have proofs in the $i$-th iterated consistency extension of $T$. I haven't looked for the answers to my questions in this book yet--I'll update the question if some of them are not answered. –  Daniel Litt Oct 30 '10 at 21:37
I don't believe it's true that $\Pi^0(T+Con(T))=\Pi^1(T)$. For instance, $\Pi^0(T)\subseteq\Pi^0(T+Con(T))$ while $\Pi^1(T)\cap\Pi^0(T)=\emptyset$ for reasonable theories. –  Henry Towsner Oct 31 '10 at 0:31
Henry, I agree. Nevertheless, I think "iterated consistency extensions" is what Daniel was really aiming for... –  François G. Dorais Oct 31 '10 at 13:15
add comment

I think you'll have to at least tweak the definition of your hierarchy, since a (strong enough) consistent theory can't prove that it doesn't prove something: $T$ can prove "$\neg Con(T)$ implies that $T$ proves every formula" (where $T$ is, say, a strong enough fragment of $PA$), so $T$ proves that "if $T$ does not prove $A$ then $T$ is consistent". And of course, if $T$ proves that it is consistent, then it isn't.

-
Fixed, I think. –  Daniel Litt Oct 30 '10 at 21:34
add comment