Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
up vote 2 down vote accepted

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.

share|cite|improve this answer
Thanks for the helpful answer. But I did not necessarily mean it to be a computable function. I am more interested in the growth rate of the maximum length of proof of statements of say length n, Can you argument be modified for that purpose ? – Mohamed Alaa El Behairy Oct 10 '11 at 18:20
Well, obviously there is a non-recursive upper bound (so long as there are finitely many formulas of a given complexity). But the point is that it grows faster than any recursive function. – Levon Haykazyan Oct 10 '11 at 21:59
Thanks a lot. This answers my question. I was thinking of that in order to show that there exists small statements that have very long proofs. thanks! – Mohamed Alaa El Behairy Oct 11 '11 at 5:56

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.