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?
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."