Provability from finite and infinite theories

Let #s be the Goedel number of s. The following fact is useful for thinking about the foundations of mathematics:

Proposition. There is a finite fragment A of Peano Arithmetic such that if T is a recursively axiomatizable theory, then there is an arithmetical formula P_T(n) such that for all arithmetical sentences s, A → P_T(#s) is a theorem of FOL if and only if T proves s.

The Proposition allows us to replace the provability of a sentence from an infinite recursive theory by the provability of a sentence from a finite theory.

Sketch of Proof of Proposition. Let M be a Turing machine that given a sentence as an input goes through all possible proofs from T and halts if it arrives at one that is a proof of the given sentence.

We can encode a history of a halting (and hence finite) run of M as a natural number such that there will be a predicate H_M(m, n) and a finite fragment A of Peano Arithmetic independent of M (I expect that Robinson arithmetic will suffice) such that (a) m is a history of a halting run of M with input m if and only if H_M(m, n) and (b) for all m and n, A proves whether H_M(m, n).

Now, let P_T(n) be ∃mH_M(m, n). Then A proves P_T(#s) if and only if there is an m₀ such that A proves H_M(m₀, n). (If A proves P_T(#s), then because A is true, there is an m such that H_M(m, #s), and then A will prove H_M(m₀, #s). Conversely, if A proves H_M(m₀, #s), then it proves ∃mH_M(m, #s).) And so A proves P_T(#s) if and only if T proves s.