Are recursive forms of Godel's statement possible?

Question

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?

Answer 1

As others have pointed out, there are certain technical difficulties with the statement of your question. To straighten them out, let's start by avoiding the use of the term "unprovable" without qualification, and be explicit about which set of axioms your statement T is supposed to be unprovable from. For instance, let's suppose that we're interested in statements T that are unprovable from PA, the axioms of first-order Peano arithmetic.

The first annoyance is that "T is true" is not expressible in the first-order language of arithmetic, by Tarski's theorem. We could get around this by working in a metatheory that is powerful enough to define the truth of an arithmetical statement, but I think for your purposes this is an unnecessarily complicated route to take. I think you're not so interested in truth per se but in provability. That is, I suspect you'd be satisfied with defining T to be Godel_0 if T is true but unprovable in PA, and defining T to be Godel_1 if T is unprovable in PA but "T is unprovable in PA" is unprovable in PA, and defining T to be Godel_2 if T is unprovable in PA and "T is unprovable in PA" is unprovable in PA but "‘T is unprovable in PA’ is unprovable in PA" is unprovable in PA, etc. That way we don't have to fuss with truth predicates.

This suffices to make your question precise, but unfortunately there is then a rather trivial solution. Take T = "PA is consistent." Then T is true because PA is consistent, and T is unprovable in PA by Goedel's 2nd incompleteness theorem. Furthermore, "T is unprovable in PA" is also unprovable in PA for a somewhat silly reason: any statement of the form "X is unprovable in PA" is unprovable in PA because "X is unprovable in PA" trivially implies "PA is consistent" (since inconsistent systems prove everything). So T is Godel_n for all n, but I don't this really gets at your intended question.

We could try to "patch" your question to avoid such trivialities, but instead let me try to address what I think is your intended question. Tacitly, I believe you are conflating the logical strength needed to prove a theorem with the psychological difficulty of proving it. That is, you interpret a result of the form "T is unprovable in X" as saying that T is somehow beyond our ability to understand. There are these monstrous conjectures out there, and we puny humans crack PA-whips or ZFC-whips or what have you at those ferocious beasts, trying to tame them. But I don't think that "T is unprovable in X" should be interpreted as meaning "T is impossible to reason about." Rather, it's just measuring a particular technical property about T, namely its logical strength. So if you're trying to come up with the über-monster, I don't think that finding something that is not only unprovable, but whose unprovability is unprovable, etc., is the right direction to go.

Finally, regarding your question about whether unprovability seems at all related to separability of complexity classes, there are some connections between computational intractability and unprovability in certain systems of bounded arithmetic. Some of this is mentioned in the paper by Aaronson that you cite; see also Cook and Nguyen's book Logical Foundations of Proof Complexity.

Answer 2

I'm not so sure about the definition of Godel_1. Can you try to formalize it a bit more?

How can you encode the formula "T is Godel_0"? For that you will need to somehow encode that "T is semantically true" without referring to notion of proof. How can you do that?

Answer 3

Godel_n statements exist for each n. You might be interested in The Unprovability of Consistency, a book by George Boolos. He defines a modal logic in which Box means "is provable," Diamond means "is consistent," and then proceeds to investigate the behavior of Godel-type sentences. (He wrote a followup book, The Logic of Provability, also.)