Let $\Phi$ be a recursively axiomatizable, consistent arithmetic theory. The unsolvability of the Entscheidungsproblem means that the set of theorems of $\Phi$ is not recursively decidable. That is, there is no algorithm that determines whether a given sentence $\varphi$ satisfies $\Phi\vdash\varphi$ or not. A proof of that fact can be found in this comment.
However, I'm interested in the proof that reduces the Entscheidungsproblem to the halting problem (which is, as far as I know, the historical proof given by Turing). The line of reasoning is that, given a Turing machine $M$ we can assign a first-order $\Sigma_1$ sentence $\varphi_M$ that states the halting of $M$ on the empty input. More explicitly, $\varphi_M$ is the sentence $\exists n H(M,n)$ where $H(M,n)$ is a first-order arithmetic formula that expresses the relation "$M$ halts (on the empty input) within $n$ steps".
Now, the proof claims that $M$ halts on the empty input if and only if $\Phi\vdash\varphi_M$. One direction is clear to me: if $M$ indeed halts, then there exists $n_0\in\mathbb{N}$ such that $\Phi\vdash H(M,n_0)$ and therefore $\Phi\vdash \varphi_M$. However, I fail to see how the second direction follows. If $\Phi\vdash\exists n H(M,n)$, it doesn't necessarily imply that there exists $n_0\in\mathbb{N}$ with $H(M,n_0)$; the promised $n_0$ might be non-standard.
Of course, this can be solved by restricting ourselves to theories $\Phi$ with $\mathbb{N}$ as a model. But I'd like to avoid that. Is there a way to overcome this problem and get a version of Turing's proof which applies to the more general case of the theory $\Phi$?
Best Answer
This is indeed not true if all you know about $\Phi$ is that it is is recursively axiomatizable, consistent, and "can express enough arithmetic" (say, in the sense of proving all of primitive recursive arithmetic).
For a counterexample: Let $G_{\mathrm{PA}}$ be the Gödel sentence for first-order Peano Arithmetic. Let $M$ be a machine that searches for a proof of $G_{\mathrm{PA}}$ from PA. Finally let $\Phi = \mathrm{PA}+\neg G_{\mathrm{PA}}$.
Since $G_{\mathrm{PA}}$ is independent of PA, we know that $M$ does not in fact terminate, and that $\Phi$ is consistent.
However, $\Phi$ thinks $G_{\mathrm{PA}}$ is false, which is to say (recalling how Gödel's construction works) that there is a proof of $G_{\mathrm{PA}}$ from $PA$. Therefore $\Phi$ will believe that $M$ does terminate -- or in less informal terms, $\Phi \vdash \varphi_M$ holds.
The claim you cite works only if we can assume that $\Phi$ is a true theory of arithmetic (meaning that $\mathbb N$ is a model) -- or at least that it is $\omega$-consistent.
(And I doubt there is any way to make the entire argument work without somehow sneaking in an assumption that sufficiently strong true theories exist in the first place. Better have that assumption out in the open).