# Turning a non-effective proof into an effective one can be arbitrarily long?

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 ?

-
Why is $F$ eventually constant if $T$ is inconsistent? In this case $\operatorname{Dec}(T,\phi)$ is always true and provable, but still with increasing $k$ we will be able to prove more and more of these and get correspondingly larger values of $c(\phi)$? – joriki Oct 3 '11 at 9:23
If $T$ is inconsistent, the proof of $T \vdash 0=1$ cen be made inside $T$. So $c(T \vdash 0=1)$ has a definite value $c_0$. But once we know that $T$ is inconsistent, we have directly $T \vdash \phi$ for any $\phi$ without needing to know anything about $\phi$, so $c(D(T,\phi))\leq c_0+c(0=1 \vdash \phi)$. – Ewan Delanoy Oct 3 '11 at 10:50
I don't see how that shows that $F$ is eventually constant. The right-hand side of the inequality contains the minimal length of something involving $\phi$, which must be at least the length of $\phi$, so for each $k$ there are only finitely many $\phi$ for which this is $\le k$? – joriki Oct 3 '11 at 11:07
@joriki : when formalizing proofs we may take $0=1 \vdash \phi$ (for any $\phi$) as a "logical axiom scheme". But you're right, this gives an upper bound of the form constant+length($\phi$) rather than a constant upper bound. – Ewan Delanoy Oct 3 '11 at 15:29

If $T$ is consistent and $\omega$-inconsistent, $T$ may prove $\operatorname{Dec}(T, \phi)$ for every $\phi$ but not actually prove every $\phi$, in which case we will have $F(k) = \infty$ for some $k$. So $F$ is not necessarily defined everywhere.
An example of such a theory if obtained by adding the statement $\operatorname{Pvbl}(0=1)$ to Peano arithmetic, in other words adding the formalization of $\mbox{PA} \vdash 0=1$'' to PA.