# Length of a Deduction

Suppose we have a sentence whose number of of symbols is less than $$n$$. Assume that this sentence is provable in Peano Arithmetic (with the first-order induction scheme).

Also, suppose that we want to code the deduction by a number less than $$g(n)$$. Are there any theorems about the length of this coding?

• Russell and Whitehead would suggest that Wiles' proof of Fermat's Last Theorem could be expressed in Peano arithmetic. How would the length of that proof compare to expressing the statement of FLT? – Matthew Daly Dec 14 '19 at 10:35

I am assuming that you are asking the following question: let $$g$$ be a function such that every sentence of length at most $$n$$ which is provable in Peano arithmetic has a proof with at most $$g(n)$$ symbols. What can we say about such a $$g$$?
The answer is that $$g$$ is not computable. In fact, any such $$g$$ can compute the halting problem. The idea is that if you know an upper bound on the proof length of some statement then checking if there is a proof is computable. Also, if $$P$$ is a program of length $$n$$ then the sentence expressing "$$P$$ eventually halts" has length at most $$h(n)$$ where $$h$$ is some computable function (in fact, for any reasonable encoding of programs, $$h$$ should be linear). So to check if $$P$$ halts, we just check if there is a proof of length at most $$g(h(n))$$ of the sentence "$$P$$ eventually halts."