What is the relationship between ZFC and Turing machine?

Question

I did not learn Logic properly but so far I understand that proof systems can be viewed as a kind of machine. For proof system, ZFC seems to be the most powerful one that we use so far. Similarly, for computation model, Turing machine seems to be the most powerful one.

So I want to ask what is the relationship between these two ? I did try to formulate the question but if it contains some misunderstanding please point it out.

Let $L$ be a language which contains all statements that can be proven in ZFC. Is $L$ decidable by Turing machine, or in other words, is $L$ computable ?

If this is true, then Turing machine is at least as powerful as ZFC proof system in the sense that, If $a \in L$, that is, $a$ can be proven in ZFC, then Turing machine can decide whether $a \in L$ as well.

For another direction, to say that ZFC system is at least as powerful as Turing machine:

Is ZFC proof system Turing-complete ?

I tried to look up for the answer, and what confuses me the most is the followings.

• ZFC is first order.
• From descriptive complexity theory, $FO=AC^0$ which is very limited.

Could you please clarify my confusion ? Thank you very much.

Answer 1

$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.

Answer 2

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.