Do the Robinson and/or Peano arithmetics suffice to prove that the Halting problem is undecidable

decidabilityelementary-set-theoryturing-machines

Robinson and Peano are both rather weak systems, but they suffice to capture the rules of the natural numbers sufficiently to talk about the Gödel numbering etc., and Kleene's T predicate indicates they can at least describe Turing machines. I would like to know if either or both of these systems suffice to prove Turing's theorem.

I think arithmetics are probably the most natural way to approach this question, which is why I focussed on them but I'd also be interested if any very weak set theories (e.g. https://en.wikipedia.org/wiki/General_set_theory) prove that Halting is undecidable.

In general I am interested in any fragment of ZF that suffices to prove undecidability of halting.

Best Answer

$\mathsf{PA}$ is vastly more than enough to prove that the halting problem is incomputable. $\mathsf{PA}$ is in fact massive overkill for the vast majority of theorems about natural numbers, or "finitary objects" (such as Turing machines, despite the infinite tape present in our intuitive conception of them) more generally.

Meanwhile, in some sense $\mathsf{Q}$ is too weak a system for the question to be meaningful. There is very little which $\mathsf{Q}$ can prove at all - e.g. it cannot prove that every number is either even or odd (= $1$ less than an even number), nor can it prove that addition is commutative. Among other things this means that intuitively-trivial modifications to definitions often wind up resulting in inequivalent versions "over $\mathsf{Q}$." For example, I don't believe that $\mathsf{Q}$ proves that $2$-tape Turing machines are no stronger than $1$-tape machines. At this point it's not clear that the question means what we want it to.


Here's a sketch of why the incomputability of the halting problem goes through in a very weak system of arithmetic. (There are various versions of the halting problem; I'll use $\{e:\Phi_e(0)\downarrow\}$, where $\Phi_e$ is the $e$th Turing machine in the standard enumeration and "$\downarrow$" means "halts," for simplicity.)

The proof boils down to basic logic + a machine construction: given a machine $\Psi$ we need to define an auxiliary machine $\hat{\Psi}$ to "defeat" $\Psi$ as a putative halting problem solver. This $\hat{\Psi}$ behaves as follows: on input $e$ it simulates $\Psi(e)$; once (if ever) this simulated computation halts, $\hat{\Psi}$ goes into an endless loop if the result is $1$ and otherwise halts and outputs $0$ (say).

So all we need is a theory of arithmetic capable of proving that the construction $\Psi\leadsto\hat{\Psi}$ actually "makes sense." Since it's an explicit construction this boils down to a totality claim, and at a glance knowing that polynomial functions are total should already be enough. So we get all the way down to theories of bounded arithmetic, which form incredibly tiny fragments of $\mathsf{PA}$.