# Turing Machines independent of ZFC

We can construct a Turing Machine M whose behavior is independent of ZFC by making it look for a contradiction in ZFC.

But I also know that if any Turing Machine does in fact halt, it can always be proved in ZFC. Therefore, if we can prove (in ZFC) that a Turing Machine's behavior is independent of ZFC, then this machine must in fact never halt.

So then, don't we "know" that M (see above) will never halt? Why is it dependent of the consistency of ZFC? It seems to me that ZFC can prove that M is independent of ZFC, and ZFC can also prove that if a Turing Machine's behavior is independent of ZFC then this machine does not halt. So why can't ZFC prove that M never halts?

I get that if ZFC were to be inconsistent, than the negation could also be proved. But isn't this the case for all theorems of ZFC? The Gödel sentences are those ones whose truth and provability depend on the consistency of the system, whereas in this case mentioned above it seems that it is only the truth (of the statement 'M never halts') that is dependent on the consistency of ZFC.

I am sure I am missing something, and would like to understand it better.

So in your next sentence, we know that $$M$$ won't halt if we know that ZFC is consistent. But we knew that anyway, by definition of $$M$$.