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


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.

  • $\begingroup$ Many thanks! Perhaps what misled me was thinking about the necessity of there being a bijection between Turing machines and formal systems that could justify Feferman's line: "talk of well-defined or effectively given formal systems can be converted into talk of Turing machines and vice versa" It seems from what you say that we could "cook up" as you say a bijective mapping Gödel numbering which gives us a bijective (perhaps even effective) map between TM and FS. The only drawback then would be that this bijection would be dependent on the particular Gödel numbering chosen. Correct? $\endgroup$ – user559507 May 7 '18 at 21:11
  • $\begingroup$ @user559507 Well, any bijection you pick is going to depend on how we choose to convert between formulas, numbers, and the strings of symbols the Turing machine operates on. There's no reason to expect a truly "notation-independent" bijection to exist, simply because we need some fixed way to compare the various types of objects we're talking about. (And yes, this does indeed give us a completely effective bijection between (codes for) machines and (codes for enumerations of) theories.) $\endgroup$ – Noah Schweber May 7 '18 at 21:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.