What is the relationship between ZFC and Turing machine?

$L$ is not computable. But it is recursively enumerable. If $\varphi$ is a theorem of ZFC, then $\varphi$ can certainly be proved by Turing machine. Just start enumerating all proofs. The problem is with sentences $\varphi$ that are not theorems of ZFC.

In the other direction, a universal Turing machine can be encoded in ZFC, indeed in far weaker theories, such as relatively small fragments of number theory.


Suppose, for reductio, that a Turing machine could decide whether the sentence with Gödel number $n$ is a theorem of ZFC. Then the property $Prov(n)$ which $n$ has when $n$ numbers a ZFC-theorem would be recursive. So there would be a ZFC wff which represents that property (since even PA can represent all recursive properties). That means there would be a wff $\mathsf{Prov}()$ such that for any $\varphi$

If ZFC $\vdash \varphi$, then ZFC $\vdash \mathsf{Prov(\ulcorner\varphi\urcorner)}$

If ZFC $\nvdash \varphi$, then ZFC $\vdash \neg\mathsf{Prov(\ulcorner\varphi\urcorner)}$

where $\ulcorner\varphi\urcorner$ is the numeral for the Gödel number of $\varphi$.

Now, by the diagonalization lemma, there would be a Gödel-style sentence $\gamma$ such that

ZFC $\vdash \gamma \leftrightarrow \neg\mathsf{Prov(\ulcorner\gamma\urcorner)}$

But we also have, by our supposition,

If ZFC $\vdash \gamma$, then ZFC $\vdash \mathsf{Prov(\ulcorner\gamma\urcorner)}$

If ZFC $\nvdash \gamma$, then ZFC $\vdash \neg\mathsf{Prov(\ulcorner\gamma\urcorner)}$

Contradiction is immediate.