Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Let's define the "difficulty" of a theorem as the logarithm of the size of its shortest proof divided by the logarithm of the size of the theorem itself. For example, if a theorem has difficulty less than 2, then it has a proof smaller than than the square of its size. (Is there a standard terminology for this or a similar concept?)

Assume the theory is consistent, effective, and essentially incomplete (e.g. PA, ZFC). Its difficulty is unbounded, because otherwise we would have an algorithm to determine provability (in NP even!), contradicting Church's theorem.

How to construct a specific sequence of theorems with increasing and unbounded difficulty? My best idea is to iteratively apply Rosser's provability predicate, but I can't figure out how to prove that this works. Any references for this or related problems?

share|cite|improve this question
I guess I didn't see your interpretation of your own question very well. Sorry for the "harsh-looking" comment. My too-quick-didn't-think-about-it answer came from a reflex ; I have a few friends who like to wikipedia too much about those logic things without understanding much of it. That "difficulty" notion seemed to me at first as a delirious notions like the many I've already heard. It now seems quite formal to me. I like Yuval's answer ; quite clear. Voted it up. I'll delete my answer. – Patrick Da Silva May 17 '11 at 4:04
up vote 5 down vote accepted

Perhaps you can use a Gödel statement stating "I am not provable with a proof of length N", where N is some huge number with a short definition.

By the way, the corresponding question for quantifier-free fragments (i.e. propositional calculus) is open - it's equivalent to NP=coNP.

share|cite|improve this answer
Aha, I see now how this works! It is much simpler than what I was trying to do. I don't yet understand the connection to NP=co-NP. – Dan Brumleve May 17 '11 at 17:50
NP=coNP iff there is a proof system that proves each propositional tautology in polynomial size. This is basically because SAT is NP-complete. – Yuval Filmus May 17 '11 at 18:31
This follows directly from the main theorem given in the wiki article Excellent and concise answer. I'm disappointed that I couldn't find the answer to the main question by myself, but the relationship to co-NP is something I might never have guessed. – Dan Brumleve May 18 '11 at 0:07

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.