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.