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

  • 3
    It is a well-defined function (for a given formal system), but it might not be com$p$utable.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$.

  • 0
    Relevant se.math question: [Upper and Lower bounds on proof length](http://math.stackexchange.com/q/71395/25554)2012-06-01