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?