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?
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!)