Let $T$ be a theory at least as strong as Peano arithmetic. We assume that we have a complete arithmetization of $T$ so that statements like $T \vdash \phi$ can be defined inside $T$, and for each $\phi$ which is decidable in $T$ we can also define $c(\phi)$, the length of the shortest proof of either $\phi$ or $\lnot\phi$ (where "length" is computed by counting the number of symbols for example). So $c(\phi)=\infty$ if $\phi$ is independent of $T$. For any given $k$, the set of proofs of length $\leq k$ is finite, and hence $\lbrace \phi | c(\phi) \leq k\rbrace$ also.
Write ${\rm Dec}(T,\phi)$ for $(T \vdash \phi) \vee (T \vdash \lnot\phi)$, i.e. ‟$\phi$ is decidable in $T$”. Suppose that $T \vdash {\rm Dec}(T,\phi)$, i.e. that we have a proof of $ {\rm Dec}(T,\phi)$ inside $T$. If this proof is non-effective, it might still leave us in the dark about which of $\phi$ or $\lnot\phi$ is true. Also, even if the proof of $ {\rm Dec}(T,\phi)$ is short, a proof of either $\phi$ or $\lnot\phi$ might be very long.
This leads us to the following definition : for any integer $k $, let
$ F(k)={\rm max}(\lbrace c(\phi) | T \vdash {\rm Dec}(T,\phi) \ {\rm and} \ c({\rm Dec}(T,\phi)) \leq k \rbrace) $
The $F$ function is everywhere defined (for large enough $k$) and computable. In the uninteresting case where $T$ is inconsistent, $F$ is eventually constant. Is $F$ primitive recursive when $T$ is consistent ?