# Lengths of proof

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.

-
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$. –  user1708 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

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$.