Does every FOL (axiom set expressible in First Order Logic) have a corresponding Turing machine?
The proved FOL statements would be strings the Turing machine accepts.
Does every Turing machine have a FOL?
The strings the Turing machine accepts are proved by a finite set of FOL axioms.
Someone said this:
Meanwhile, FOL (unlike propositional logic) is Turing-complete in an appropriate sense
(See comments on https://math.stackexchange.com/a/3635100/187128)