For the same reason, there is no computable function f such that for every provable sentence x the shortest proof of x has length at most f(x). This is because we can use such an f to determine whether or not a given sentence is provable, simply by checking all proofs of length at most f(x).
