3
$\begingroup$

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.

  • 4
    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.2012-05-31
  • 0
    The 20 or so commonly used. Including $\forall$ and $\exists$.2012-05-31
  • 2
    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.2012-05-31
  • 0
    The question does seem to be well-posed. Take a theory, say PA. Generate all proofs of length 1; take the final step from each; the length of the shortest of these is $f(1)$. Now generate all proofs of length 2; take the final step from each; discard those that appeared in step 1; the length of the shortest one remaining is $f(2)$. Repeat ad lib.2012-05-31
  • 3
    @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)$.2012-05-31
  • 0
    Yes, you're right. It's ill-posed as written. Still there is something that the OP is getting at that I think can be reasonably discussed.2012-05-31
  • 3
    It is a well-defined function (for a given formal system), but it might not be computable.2012-05-31

1 Answers 1

7

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

  • 2
    [Relevant](http://plato.stanford.edu/entries/goedel/#SpeUpThe): "Theorem 5: Given any recursive function f there are provable sentences φ of arithmetic such that the shortest proof is greater than f(⌈φ⌉) in length."2012-05-31
  • 0
    Relevant se.math question: [Upper and Lower bounds on proof length](http://math.stackexchange.com/q/71395/25554)2012-06-01