Solomon Feferman, at page 138 of his 2006 paper "Are there absolutely unsolvable problems" says that each formal system of axioms can be made to correspond to a suitably designed Turing machine so that
[...] with each effectively given formal system is associated a Turing machine $M$ which enumerates the set of theorems of $S$, or—more picturesquely—prints out the theorems of S one after another.
I have omitted the argument he gives for this because I don't find it problematic. Then he continues
Conversely, given any formal language $L$, any Turing machine $M$ can be made to correspond to a formal system $S$ in $L$ by extracting from the numbers it enumerates those that are Gödel numbers of formulas of $L$, and taking their deductive closure to be the theorems of $S$. In this way, talk of well-defined or effectively given formal systems can be converted into talk of Turing machines and vice versa.
Question: Is the former an informal although correct argument that can be given for the identity between Turing machines and formal systems?
My problem with this informal argument is the following: if we take from all the numbers $M$ enumerates, only the deductive closure of those formulae that correspond to Gödel numbers in a given language $L$, what about those numbers which do not correspond to any Gödel number? How are they going to be accounted for in the formal system that supposedly corresponds to $M$?
It seems to me that such numbers are simply ignored by this argument, and that perhaps a more direct argument which says more about the rules of inference would be best suited in this case. But maybe there is something I'm missing here...