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 ?

  • 1
    $\begingroup$ 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)$? $\endgroup$ – joriki Oct 3 '11 at 9:23
  • $\begingroup$ 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)$. $\endgroup$ – Ewan Delanoy Oct 3 '11 at 10:50
  • 1
    $\begingroup$ 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$? $\endgroup$ – joriki Oct 3 '11 at 11:07
  • $\begingroup$ @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. $\endgroup$ – 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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.