# Are recursive forms of Godel's statement possible?

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?

• This may be more suitable for the logicians at MO -- feel free to indicate if this is the case. Aug 17, 2010 at 6:15

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.

• Indeed, your trivial example does resolve the question, and I'm glad to see that it had such a simple resolution -- I had suspected that such statements were probably equivalent. However I am only interested in logical strength, not the psychological difficulty of proving or reasoning about things. The intent of my question was to ask, "is it ever formally harder to demonstrate the unprovability of a statement's unprovability than it is to show a statement is unprovable?" Your example seems to suggest the answer is "no". Jan 7, 2011 at 17:43
• I don't fully understand your rephrased question, because you're still using the word "unprovable" without qualification. Say T1 is unprovable in X1. Then "T1 is unprovable in X1" (call this statement T2) is provable in some systems and not others. Are you interested in the (un)provability of T2 in X1 itself or in some other system X2? If the latter, then in general there will exist systems X3 that prove T2 but not "T2 is not provable in X2." Jan 20, 2011 at 22:39

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?

• Excellent point. The notion of Truth is impossible to encode in a consistent "strong enough" logic. Aug 17, 2010 at 13:46
• As you suggest, I'm not so sure the statement can be formalized without explicitly defined notions of truth and provability. I assume it's evident what I mean in an informal sense: a statement T is Godel_1 iff the statement "T is true, but unprovable" is true, but unprovable. If Godel's sentence is, loosely, "No proof of this theorem exists", then a Godel_1 sentence might be, "No proof of the theorem 'no proof of this theorem exists' exists"." This doesn't quite capture the precise notion of the inner statement being true, however. Aug 17, 2010 at 20:48

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.)

• Could you elaborate on Boolos's results? Does he prove that such statements exist? Aug 17, 2010 at 16:21
• Argh. I read the first book, not the second one, but that was a million years ago when I thought I was going to do logic when I grew up. I even sold my copy of the book to a bookstore. I might check to see if it's in the library here. If I looked at it again, I could probably remember things reasonably fast. No promises though, and sorry I'm not more help. Aug 17, 2010 at 16:34