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?
 A: 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.
