Upper and Lower bounds on proof length

Question

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.

Answer 1

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.

Answer 2

With and upper bound of length l you can search for all proofs of length less then l, which will terminate in finite time. So you could solve the halting problem say, in finite time, which is impossible. For lower bound, check all combinations less then length j, as long as you want.