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?
1 Answer
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$.
-
$\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