Problem Detail:
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.
Asked By : vzn
Answered By : David Richerby
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/18424
