Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

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 $f(n)$ be the length of the shortest statement whose shortest proof has length $n$ or more.

What are the asymptotics of $f(n)$? With standard symbols and length counted by character.

For any standard theory, such as PA or ZFC.

share|cite|improve this question
This question does not make sense until you specify what symbols you're using, what axioms you're using, and what proof rules you allow. – Qiaochu Yuan May 31 '12 at 1:12
The 20 or so commonly used. Including $\forall$ and $\exists$. – TROLLKILLER May 31 '12 at 1:14
OP said you could pick any standard theory, and offered PA and ZFC, which are quite different, so I presume that means that the answerer will get to decide, as OP is not planning to be fussy about the details. I think it's a fair question. – MJD May 31 '12 at 1:31
@MarkDominus: If it said "the length of the shortest statement whose shortest proof has length exactly $n$", that would work. But it said "$n$ or more". So there might be a statement of length 2 whose shortest proof has length 76576428414812. You won't know this until you enumerate the proofs of length 76576428414812. And if there is a statement of length 2 that is unprovable, you may never know that it isn't counted in $f(2)$. – Robert Israel May 31 '12 at 1:46
It is a well-defined function (for a given formal system), but it might not be computable. – Robert Israel May 31 '12 at 1:53
up vote 7 down vote accepted

In any theory to which Gödel's theorems apply, this is going to grow extremely slowly, in the following very strong sense. Suppose $g(m)$ is a function such that for any positive integer $m$, $f(g(m)) > m$. Then given a statement $S$ of length $\le m$, if $S$ is provable the shortest proof of $S$ must have length at most $g(m)$. But then $g(m)$ can't be a computable function (otherwise we could test whether $S$ is provable by enumerating all proofs of length at most $g(m)$, and we'd have an algorithm for solving the Halting Problem).

Putting it another way, for any computable function $g: {\mathbb N} \to {\mathbb N}$, there is some $m$ such that $f(g(m)) \le m$.

share|cite|improve this answer
Relevant: "Theorem 5: Given any recursive function f there are provable sentences φ of arithmetic such that the shortest proof is greater than f(⌈φ⌉) in length." – MJD May 31 '12 at 2:15
Relevant se.math question: Upper and Lower bounds on proof length – MJD Jun 1 '12 at 16:49

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.