Is the set of Turing Machines decidable in ZFC non-recursive?

Let S be the set of all the TMs which halting is decidable in ZFC (for each TM in S, we can find one algorithm in ZFC that determines whether the machine halts or not). Is S recursive? Is there one algorithm that can enumerate both the stopping and non-stopping machines of S?

For example, would the set of Diophantine equations still be non-computable if we removed those instances that are independent of ZFC?

Assume $$\mathsf{ZFC}$$ is $$\Sigma^0_1$$-sound.

For each sentence $$\varphi$$ in the language of set theory, consider the machine $$T_\varphi$$ which - regardless of input - searches for a $$\mathsf{ZFC}$$-proof or disproof of $$\varphi$$ and halts iff it finds one. Then $$T_\varphi$$ halts iff $$\varphi$$ is $$\mathsf{ZFC}$$-decidable, and $$\mathsf{ZFC}$$ proves this.

Since $$\mathsf{ZFC}$$ is $$\Sigma^0_1$$-complete, if $$T_\varphi$$ halts (on input $$0$$, say) then $$\mathsf{ZFC}$$ proves that $$T_\varphi$$ halts. What if $$T_\varphi$$ doesn't halt? Well, then $$\mathsf{ZFC}$$ can't prove that $$T_\varphi$$ does halt by the soundness assumption above, and by the last four words of the previous paragraph + Godel's second incompleteness theorem $$\mathsf{ZFC}$$ can't prove that $$T_\varphi$$ doesn't halt either (otherwise $$\mathsf{ZFC}$$ would prove that $$\mathsf{ZFC}$$ is consistent).

So the halting status of $$T_\varphi$$ is $$\mathsf{ZFC}$$-decidable iff $$\mathsf{ZFC}$$ decides $$\varphi$$. But it's a standard exercise that the set of $$\mathsf{ZFC}$$-decidable sentences isn't computable, since otherwise we could build a computable consistent complete extension of $$\mathsf{ZFC}$$ contradicting the first incompleteness theorem.

• Perfect, thanks! May 9 at 3:15
• Does the fact that the set of ZFC-decidable sentences is not computable also implies that the set of Diophantine equations that are decidable in ZFC is not computable? I assume this must be right because of the equivalence between Turing Machines and Diophantine equations, but I would like to confirm. May 15 at 4:40
• @CharbelBejjani Yes, that's correct. May 15 at 4:41
• @CharbelBejjani Yes, we can brute-force-search through $\mathsf{ZFC}$-proofs and so computably enumerate the set of machines which $\mathsf{ZFC}$ proves halt on input $0$ (say). Using the same logic we can computably enumerate the set of machines which $\mathsf{ZFC}$ proves don't halt on input $0$ (say). However, this doesn't contradict the fact that the set of theorems of $\mathsf{ZFC}$ is non-computable. What's going on here is the distinction between computable and computably enumerable: the set of $\mathsf{ZFC}$ theorems is computably enumerable. Jun 7 at 3:40
• @CharbelBejjani If by "solve" you mean "determine whether they are solvable," yes. However, note that the set of such equations isn't computable. Jun 7 at 5:41