It is well known the analogy between formal systems and Turing machines. If I am not wrong, you can code any formal system of language L in first order logic into a Turing machine, and there is a bijection between the formulas that are provable in the formal system and the programs that halt. If the formal system is PA, the analogy goes beyond what is computable or provable, and extends into the transfinite: by Post's theorem there is an equivalence between the arithmetical hierarchy (that is, the set of first order formulas of PA) and the finitely iterated Turing jumps of the empty set. The analogy can even be extended to second order arithmetic by using infinitely iterated Turing jumps (or equivalently, infinite time Turing machines).
Question: Is this extension (that is, similarity between provability and computation into the transfinite) valid only for PA, or is also valid for any formal system in a first order language?