3
$\begingroup$

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 ?

  • 0
    @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.2011-10-03

1 Answers 1

2

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.