# A Turing machine for which halting is outside ZFC

If, given Turing machine T, "T halts" or "T doesn't halt" could be derived from axioms of ZFC, halting problem would be in R. As it isn't, there must exist a Turing machine for which truth or falsehood of halting is independent of ZFC.

I want to see it. Is such machine known?

• What do you mean by "the halting problem would be in RE. As it isn't..." Usually, we show the set of halting programs is r.e. but it is not recursive. Functions are not called "r.e.", sets are, and the set of halting turing machines is definitely r.e. Commented Aug 3, 2013 at 13:15

Let $T$ be the Turing machine which looks for a proof of a contradiction in ZFC. If ZFC is consistent, then whether or not $T$ halts will be independent of ZFC. (Indeed, if not, then this would contradict Gödel's incompleteness theorem!)
• No, if ZFC is consistent, then $T$ won't halt. Commented Aug 3, 2013 at 13:43
• @PyRulez I think the deal is that, in ZFC+$\lnot$Con(ZFC), there are sets that the model thinks are finite but are actually infinite. The reason the model thinks they're finite is because a set is infinite iff there's an injection from it to a proper subset of itself, and injections are types of sets. So the model thinks the "finite" set is finite because the required injection isn't in the model. In any case, $\lnot$Con(ZFC) means there's a natural number that codes a proof of a contradiction in ZFC. There is, it's just that the "number" is infinitely big. Commented Aug 7, 2015 at 3:39
• And the machine $T$ will halt, it just takes a "finite" (infinite) amount of time. Commented Aug 7, 2015 at 3:40