Examples of provably${}^n$ unprovable statements Given any statement $A$ and a classical theory $T$ which we assume is at least as strong as Peano Arithmetic ($\sf PA$), we have that $T\vdash A$ implies $T\vdash T\vdash A$ (that is, if a statement is provable, then it is provably provable). Let $T_1=T$ and $T_{n+1}=T_n+{\sf Con}(T_n)$. (We need stronger theories if we want to prove unprovability.) Given this, simply by considering the truth values of the relevant statements, we get the following classification of statements by unprovability:


*

*$T\vdash A$ ($A$ is provable)

*$T_2\vdash T\not\vdash A$ ($A$ is provably unprovable)

*$T_3\vdash T_2\not\vdash T\not\vdash A$ ($A$ is provably unprovably unprovable)
    ...
    $\omega$. For all $n$, $T_n\not\vdash\dots \not\vdash T_2\not\vdash T\not\vdash A$ (we can't say anything about $A$'s provability)
We can refine this hierarchy by also considering the status of $\lnot A$. Let's call a class $m,n$ statement one such that $A$ is at level $m$ above and $\lnot A$ is level $n$ in the list. Since $T\vdash\lnot A$ implies $T_2\vdash T\not\vdash A$, the only nonempty classes at level $1$ are the class $1,2$ statements (provable statements) and the class $2,1$ statements (refutable statements). Independent statements are in class $2,2$. The class $1,1$ is nonempty iff the theory is inconsistent.
My question is: Are there any (preferably "natural") statements that fall further into this hierarchy? I know many examples of independent statements, like the continuum hypothesis or the axiom of choice relative to $\sf ZF$, or the Paris–Harrington theorem relative to $\sf PA$. But I know no examples of even any class $2,3$ statements. I expect there may also be natural examples of $\omega,\omega$ statements. My guess is that all the classes $m,n$ with $m,n\ne1$ are nonempty, but examples elude me.
 A: [This is a partial answer, but I decided to post it anyway since no one else has answered for a long time now. Very interesting question by the way!]
Note that if $T = PA + \neg Con(PA)$, then $T \vdash \neg Con(T)$ and hence $T_2$ is inconsistent and proves everything, so your hierarchy collapses. So it's not enough just to assume that $T$ contains $PA$. I think you need the much stronger condition of assuming that $T$ is arithmetically sound, namely that every arithmetical statement that $T$ proves is true for $\mathbb{N}$. This would happen if for example $T$ has an $ω$-model, namely that there is a model of $T$ where the arithmetical part is $\def\nn{\mathbb{N}}$$\nn$. If the language of $T$ is the language of arithmetic (with no extra symbols), then these two notions are equivalent and just mean that $\nn$ satisfies $T$, but in general arithmetic soundness is weaker.
So we shall from now assume that $T$ has decidable proof validity and is arithmetically sound. Note that by induction $T_n$ is arithmetically sound for every $n \in \nn$.
Let $D(n)$ denote the class of sentences at level $n$ in your hierarchy, and let $D(m,n)$ denote your class $m,n$. And let $D^*(k,l) = \bigcup \{ D(m,n) : k \le m \le ω \land l \le n \le ω \}$.
Firstly, your statement that independent sentences are in $D(2,2)$ is not correct, because all you know is that it is in $D^*(2,2)$, since the very definition of independence is equivalent to being in $D^*(2,2)$. Note that our entire discussion is in some meta-system, usually taken to be ZFC. The question of whether or not a sentence over $T$ is independent over $T$ has a fixed truth-value in the meta-system. Even if we cannot prove some sentence independent, it does not change which class it falls in.

Some sentence over $T$ is in $D^*(2,3)$.

Claim: $Con(T_2) \notin D(1)$. Proof: If $T_1 \vdash Con(T_2)$ then $T_1 \vdash Con(T_1)$, which gives a contradiction.
Claim: $( \neg Con(T_2) ) \notin D(1)$. Proof: If $T_1 \vdash \neg Con(T_2)$, then $T_1 \vdash ( T_1+Con(T_1) \vdash \bot )$, and hence $T_1 \vdash ( T_1 \vdash \neg Con(T_1) )$, but by arithmetical soundness this implies $T_1 \vdash \neg Con(T_1)$, which gives a contradiction.
Claim: $( \neg Con(T_2) ) \notin D(2)$. Proof: If $T_2 \vdash ( T_1 \nvdash \neg Con(T_2) )$, then $T_2 \vdash Con( T_1 + Con(T_2) )$, and hence $T_2 \vdash Con(T_2)$, which gives a contradiction.
Claim: $Con(T_2) \in D(2)$. Proof: $T_2 \vdash ( T_1 \nvdash Con(T_1) )$, and hence $T_2 \vdash ( T_1 \nvdash Con(T_2) )$.
Conjecture: $( \neg Con(T_2) ) \in D(3)$.
Therefore $Con(T_2) \in D^*(2,3)$, and I think it is in $D(2,3)$.
I also think that there is some sentence $φ$ over $T$ that is in $D^*(ω,ω)$, but don't see why.
