# Unbounded minimal $T$-proof lengths and $T$-provably total functions

Let $$T$$ be a sound, r.e. theory containing elementary arithmetic. Fix a $$T$$-proof predicate $$\mathrm{Proof}_T(x,y)$$. Let $$\phi(x)$$ be such that, for all $$n$$, $$T\vdash\phi(n)$$; $$\forall x\,\phi(x)$$ is true but $$T$$ does not prove it. Define $$f(n)$$ as the minimal length of the $$T$$-proof of $$\phi(n)$$ (i.e. $$f(n)$$ is the minimal $$m$$ such that $$\mathrm{Proof}_T(m,\ulcorner\phi(n)\urcorner)$$). Suppose $$f$$ is unbounded. Must $$f$$ dominate all $$T$$-provably total functions?

No, such an $$f$$ can grow extremely slowly.
Let $$\varphi$$ be a formula such that for each $$n$$, we have $$T\vdash\varphi(n)\leftrightarrow$$ "there is no $$T$$-proof of $$\varphi(n)$$ of length $$." The existence of such a formula follows from (the proof of) the diagonal lemma. As long as $$T$$ is consistent, no $$n$$ can have $$\varphi(n)$$ be $$T$$-provable in length $$ (since then $$T$$ could verify such a proof, which - combined with the above $$T$$-provable equivalence and the hypothesized proof - would yield a contradiction in $$T$$). But this means that $$T$$ does prove $$\varphi(n)$$ for each $$n$$ by brute-force-search (which is roughly exponential in length).