The self-referentiality of the P/NP problem has sometimes been highlighted as a barrier to its resolution, see, for instance, Scott Aaronson's paper, is P vs. NP formally independent? One of the many conceivable resolutions to P/NP would be a demonstration that the problem is formally independent of ZFC or true but unprovable.
It's conceivable that the self-referentiality of the problem can pose a deeper challenge in proofs of independence, for example, if statements about its provability are themselves unprovable or otherwise impossible to reason about.
Suppose we call a theorem T Godel_0 if it is true but unprovable in the sense of Godel's theorem. Call T Godel_1 if the statement "T is Godel_0" is true, but unprovable. Call T Godel_i if the statement "T is Godel_{(i-1)} is true.
We know that Godel_0 statements exist, and a few examples have been found "in the wild" that are not constructed explicitly for this purpose, as in this article.
My question is: do there exist any Godel_1 statements or higher? Are such statements a natural consequence of Godel's theorem?
What about a statement about which we can prove absolutely nothing: ie, one for which for every k > 0, T is Godel_k?
I can ask an analogous question for formal independence, although I suspect the answer is "no" there.
To return to the P vs. NP question, let me ask whether there's even a hint that Godel's theorem is relevant to questions of class separability. Have any true but unprovable statements been identified with respect to complexity classes -- beyond, of course, the obvious connection between halting problem and Godel's theorem?