# Construction of a sequence of theorems with increasing and unbounded “difficulty”?

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?

-
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