Is there a particular Turing Machine whose halting is independent even from Gödel propositions of ZFC?

Question

I know that there are some set of Diophantine equations that have no solutions, and yet this is undecidable in ZFC. However, from what I understood, one must only assume that ZFC is consistent to see that they indeed have no solutions. My question is: is there a particular set (or sets) of Diophantine equations that is (are) undecidable in ZFC and does (do) not even depend on the consistency of ZFC (somewhat like the Continuum Hypothesis)?

Answer 1

Rather than talk about Turing machines or Diophantine equations specifically, I'll just talk about $\Pi^0_1$ sentences. These are sentences of the form $\forall x\theta(x)$, where $\theta$ is a formula of arithmetic using only bounded quantifiers; we can always choose to represent $\Pi^0_1$ sentences as non-halting statements (essentially trivially), consistency statements (ditto), or Diophantine unsolvability statements (via the MRDP theorem), but this makes the situation look more complicated than it is.

It's easy to see that (under reasonable assumptions of course) there are $\Pi^0_1$ sentences independent of $\mathsf{ZFC+Con(ZFC)}$ - for example, just consider $\mathsf{Con(ZFC+Con(ZFC))}$. More generally, we can "iterate" the second incompleteness theorem. Interestingly, in a sense we can reduce every $\Pi^0_1$ sentence to $\mathsf{Con^\alpha(ZFC)}$ for some $\alpha$; there's a lot of technical detail here that I'm ignoring, but see the book "Inexhaustibility" by Franzen. Meanwhile, sentences like $\mathsf{CH}$ are totally different: they lie beyond the arithmetical hierarchy, and can't be reached by any sort of iterated consistency process at all.

So in a sense, Diophantine/Turing machine facts can't get too far beyond mere consistency of $\mathsf{ZFC}$.