Every Turing machine corresponds to a formal system

Question

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...

Answer 1

I think this is ultimately a non-issue (which is not to say that this is a silly question!).

Note that we could choose to use a method of Godel numbering which is surjective - that is, in which every number corresponds to a well-formed formula. This is not the one Godel introduced, and takes a bit of work to cook up, but is perfectly okay (and in particular is itself computable in the obvious sense). This gives a very snappy translation between Turing machines and formal systems. The motivation for "throwing away" nonsensical numbers when we're using other numberings, then, is to make the translation appropriately independent of the specific numbering we use.

Conversely, this means that we should only be worried about throwing away the nonsensical numbers if we actively want to work with a non-surjective numbering. At that point, how we should treat nonsensical numbers will come down to why we want to work with such a numbering in the first place, and without that I think there's no way to guess what the right action would be.

The only real objection I see to throwing out the nonsensical numbers is that it makes multiple machines correspond to the same system. I don't think that's a drawback, though, since the same formal system will have lots of equivalent axiomatizations (let alone effective enumerations of axioms)! Indeed, redundancy is often an unavoidable part of computability theory, and there are even situations where the absence of redundancy is pathological.