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.