# Is there a TM that halts on all inputs but that property is not provable?

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.

• 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. – David Richerby Nov 28 '13 at 16:04
• 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... – vzn Nov 28 '13 at 16:14
• 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. – cody Dec 3 '13 at 20:03

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.

• 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. – cody Dec 3 '13 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$.