Suppose we have fix some interpretation of propositional (not first-order!) logic inside PA, and say $f(n) = $ {the maximum length of a proof of a tautology with $n$ propositional primitives}
Questions:
1) Is this PA-definable? I think so, because all of the deduction rules of propositional logic are codeable as PA relations.
2) Does PA prove that this function is total a priori? We know there is some sort of exponential bound (convert everything into CNF, and then inspect the result), but can we prove that this function is PA-computable without knowing there exists a bound necessarily?
Motivation: I want to bound the length of proofs of tautologies of length $n$. While one can do this by considering carefully the proof of Completeness for propositional logic, this is quite tedious, and I was wondering whether we can justifiably bound this function by, say, the Goodstein function (or some other similarly fast-growing function).
Yes, $PA$ can prove that the "propositional busy beaver" is total. In fact, the bound you cite is provable in $PA$ - the standard proof doesn't use anything beyond $PA$!