2
$\begingroup$

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?

  • 0
    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.2011-05-17

1 Answers 1

5

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.

  • 0
    This follows directly from the main theorem given in the wiki article http://en.wikipedia.org/wiki/Co-NP. 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.2011-05-18