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$?

  • $\begingroup$ See Boolos, Burgess & Jeffrey, Ch.11 The Undecidability of First-Order Logic. $\endgroup$ Mar 31 at 13:58

Now, the proof claims that $M$ halts on the empty input if and only if $\Phi\vdash\varphi_M$.

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).

  • $\begingroup$ It appears quite circular proof. To prove the system consistent or $\omega$ consistent we use system that basically assumes it is consistent. A lot like the model theoretic proof of consistency of $PA$. $\endgroup$
    – Dole
    Mar 31 at 14:44

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.