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 hierarchy 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 hierarchy, 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 hierarchy 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](http://video.ias.edu/voevodsky-80th) 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.



What is the depth of the "provability hierarchy"?
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](http://books.google.com/books?id=6gJa6bjf374C&lpg=PP1&ots=5jv2Db6sxZ&dq=inexhaustibility&pg=PA185#v=onepage&q&f=false). See also this [related question](https://mathoverflow.net/questions/12865/using-consistency-to-create-new-axioms-in-set-theory) and this [blog article](http://xorshammer.com/2009/03/23/what-happens-when-you-iterate-godels-theorem/) by Mike O'Connor.


