Does there exist a Turing machine that halts on all inputs but that property is not provable for some reason?

I am wondering if this question has been studied. Note, "unprovable" could mean a "limited" proof system (which in the weak sense think the answer must be yes). I am of course interested in the strongest possible answer, i.e. one that is not provable to halt on all inputs in say ZFC set theory or whatever.

It occurred to me this could be true of the Ackermann function but I am hazy on the details. It doesn't seem like Wikipedia describes this aspect clearly.

  • 5
    $\begingroup$ Peano Arithmetic is enough to prove that Ackermann's function is total: this is exercise 17 of Jaap van Oosten's Introduction to PA notes. $\endgroup$ Nov 28, 2013 at 16:04
  • $\begingroup$ total computable fn defn wikipedia. note this question was partly motivated by looking into the collatz fn where it is a related long open question... $\endgroup$
    – vzn
    Nov 28, 2013 at 16:14
  • 2
    $\begingroup$ This is a silly remark, but note that for every Turing machine M that terminates on all input, the theory $\mathrm{PA}+\mbox{"$M$ terminates on all input"}$ is a consistent theory. But using Gödels theorem we can show that there is no single recursive theory that can prove the termination of all such machines. $\endgroup$
    – cody
    Dec 3, 2013 at 20:03

4 Answers 4


Yes. The Turing machine that computes the Goodstein sequence beginning from its input and terminates when the sequence hits zero. It always terminates but this can't be proven in Peano arithmetic. I'm sure there are equivalent things for ZFC or any other system you might choose.

Edit For ZF, Hartmanis and Hopcroft show that there's a Turing machine $M$ that rejects every input but that this can't be proven in ZF. I'm not sure if ZF can prove that $M$ always halts but it certainly can't prove that the machine $M'(x)$ $=$ "If $M$ accepts $x$ then loop forever, else halt" always halts, even though it does. That still leaves ZFC open but ZF is more powerful than PA.

See Sec. 3 of Scott Aaronson's survey on independence of P=NP for an exposition of the Hartmanis–Hopcroft result and citations to their original papers.

  • $\begingroup$ About adding the choice axiom: ZFC can't do better than ZF for "simple" statements like a halting problem (in this case $\Pi^0_2$ if I'm not mistaken). This is because ZF and ZFC prove exactly the same $\Pi^0_2$ statements. $\endgroup$
    – cody
    Dec 3, 2013 at 18:59

Take a theory ${\cal T}$ that is at least as strong as "basic" arithmetic, and that is recursively enumerable (it's possible to enumerate every theorem of ${\cal T}$).

Construct the following machine $M$, which behaves as following on input $n$:

If there is no proof of 0 = 1 in less than n steps in T, ACCEPT
Otherwise, LOOP.

It's pretty easy to show using the second incompleteness theorem that ${\cal T}$ can not prove that $M$ terminates on all input (iff it is consistent).

This of course works for ${\cal T}=\mathrm{ZFC}$, ${\cal T}=\mathrm{PA}$, ${\cal T}=\mathrm{PA²}$,... as long as they are consistent.


Some unprovable in PA but true theorems can be converted to Turing machines. For example, there is a (strengthened version of) Ramsey's theorem, that is unprovable in PA, and we can construct a machine that would just search for the right $N$.


The halting of one TM can be encoded by constructing another TM and asking whether it halts. That is, given TM $T_1$ and input $I_0$, we can construct a TM $T_2$ with inputs indexed by the natural numbers such that $T_2(I_n)$ halts if $T_1(I_0)$ doesn't halt after $n$ steps. Then there are inputs on which $T_2$ doesn't halt iff $T_1(I_0)$ does halt, and proving that $T_2$ halts on all inputs is equivalent to proving that $T_1(I_0)$ doesn't halt. Thus, once we find $T_1, I_0$ such that $T_1(I_0)$ doesn't halt, but it is not provable that it doesn't halt, there must be a $T_2$ that halts on all inputs, but it is not provable that it halts on all inputs.


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.