2
$\begingroup$

Let a formula $\phi$ of the language of first-order Peano arithmetic be total in a theory Th that extends PA iff, for any $k_1, \dots, k_n \in \omega$, Th $\vdash \phi(\bar k_1, \dots, \bar k_n)$ or Th $\vdash \neg \phi(\bar k_1, \dots, \bar k_n)$. Is it true that total formulae in Th are provably equivalent in Th to $\Delta_0$ formulae?

$\endgroup$

1 Answer 1

5
$\begingroup$

No.

Certainly the statement is false for arbitrary theories.

For computably axiomatizable theories, it's still false; what follows is informal. Consider a uniformly computably axiomatizable sequence of theories $T_i$ which are independent: if I have a finite set $\{\varphi_i: i<n\}$ of formulas with each $\varphi_i$ either of the form $Con(T_i)$ or $\neg Con(T_i)$, then the conjunction of those formulas does not prove $Con(T_{n})$ or $\neg Con(T_{n})$.

Now let $Th$ be the theory gotten from PA by adjoining the axioms "$Con(T_i)$" for each $i\in\omega$. Then $Th$ is consistent and computably axiomatizable, and the formula $Con(T_x)$ is total in $Th$, but not provably $\Delta^0_1$.

And this can even be extended to finitely axiomatizable theories: take $$Th=PA+\neg Con(PA)+\forall x(Con(T_x)\text{ unless there is a $PA$-proof of 0=1 of length $<x$})$$ for appropriate choice of $T_i$.

$\endgroup$
7
  • $\begingroup$ If Th is recursively axiomatisable, is there a $\Sigma_1$ formula in the language of the theory that defines totality? $\endgroup$ Jan 21, 2015 at 0:37
  • 1
    $\begingroup$ No. Consider the formula $\psi_T(x)=$"Either there is no proof that $T$ is inconsistent of length $<x$, or $PA$ is consistent" as $T$ ranges over finitely axiomatizable theories. Then $\psi_T(x)$ is $PA$-total iff $T$ is consistent, so if totality were c.e., the consistency of finitely axiomatizable theories would be computable. $\endgroup$ Jan 21, 2015 at 0:45
  • 1
    $\begingroup$ Basically, as a rule of thumb, anything defined in terms of "true" $\omega$ (as totality is) is going to be poorly behaved, model-theoretically . . . $\endgroup$ Jan 21, 2015 at 0:46
  • $\begingroup$ But in PA you can. I'd like to have it specifically in PA + $\forall x(Bew\ (\neg x) \rightarrow \neg Bew(x))$. Is there a counterexample too? $\endgroup$ Jan 21, 2015 at 1:09
  • 1
    $\begingroup$ I'm sorry, I don't quite understand: in the phrases "in PA you can [???]" and "I'd like to have [???] specifically in . . .", it's not clear to me what you are referring to. For what it's worth, the argument I've given shows that for any "reasonable" theory $T$, the set of $T$-total formulae is not c.e., which is very general . . . $\endgroup$ Jan 21, 2015 at 5:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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