How fast does the Godel speed-up theorem proof length grow?

332 Views Asked by At

Godel's speed-up theorem states that are theorems with arbitrarily long proofs (and can be arbitrarily shortened by working in a more powerful system).

Let $g(n)$ be defined as the number of symbols in the shortest proof of "This statement cannot be proved in Peano Arithmetic in less than n symbols"

$g(n)=\Omega(n)$, since any proof of the statement for $n$ would lead to a contradiction in PA.

$g(n)=\mathcal O (e^n)$, since you can proof the $n$th statement by simply listing all proofs under $n$ symbols (of which there are exponentially many) and noting that none of them prove the statement (and we established that none of them do since they would lead to an inconsistency in PA). This argument in particular means that $g(n)$ is defined for all $n$.

So the growth rate of $g$ lies between linear and exponential. Can we more precisely pinpoint its growth rate? (For example, could we say that $g(n)=\Theta(n^x)$ for some $x$?)