# Upper and Lower bounds on proof length

Given a First Order language say, for arithmetic $\langle 0, 1, +,\cdot ,^\wedge, S \rangle$, Can one establish any lower or upper bounds on the length of proofs from certain recursively enumerable set of axioms, say PA, of a statements expressed in terms of a metric of the statements complexity, say length or quantifier depth or number of variables? Thanks.

-

Assume you have a recursive function $f$ taking a formula into an upper limit of the length of its proof in $PA$. Then you can decide provability in $PA$. Indeed, given a formula $\phi$, there are finitely many strings of length less then or equal to $f(\phi)$. Simple check whether any of these strings represents a proof of $\phi$. This argument applies equally to any recursive enumerable set of axioms, where provability is undecidable.
For the lower bound, one obvious answer is $0$, this won't be of much use however.