Free Gödel, Escher, Bach: An Eternal Golden Braid by Douglas R. Hofstadter Page B

and this gives hope that one way or another, MU could be produced. It might involve lengthening the string to some gigantic size, and then extracting piece after piece until only two symbols are left; or, worse yet, it might involve successive stages of lengthening and then shortening and then lengthening and then shortening, and so on. But there is no guarantee it. As a matter of fact, we already observed that U cannot be produced at all and it will make no difference if you lengthen and shorten till kingdom come.
    Still, the case of U and the case of MU seem quite different. It is by very superficial feature of U that we recognize the impossibility of producing it: it doesn't begin with an M (whereas all theorems must). It is very convenient to have such a simple way to detect nontheorems. However who says that that test will detect all nontheorems?
    There may be lots strings which begin with M but are not producible. Maybe MU is one of them. That would mean that the "first-letter test" is of limited usefulness able only to detect a portion of the nontheorems, but missing others. B there remains the possibility of some more elaborate test which discriminates perfectly between those strings which can be produced by the rules and those which cannot. Here we have to face the question,
    "What do mean by a test?" It may not be obvious why that question makes sense, of important, in this context. But I will give an example of a "test" which somehow seems to violate the spirit of the word.
    Imagine a genie who has all the time in the world, and who enjoys using it to produce theorems of the MIU -system, in a rather methodical way. Here, for instance, is a possible way the genie might go about it

    Step 1: Apply every applicable rule to the axiom MI. This yields two new theorems MIU, MII.
    Step 2: Apply every applicable rule to the theorems produced in step 1. This yields three new theorems: MIIU, MIUIU, MIIII .

    Step 3: Apply every applicable rule to the theorems produced in step 2. This yields five new theorems: MIIIIU, MIIUIIU, MIUIUIUIU, MIIIIIIII, MUI.

    This method produces every single theorem sooner or later, because the rules are applied in every conceivable order. (See Fig. 11.) All of the lengthening-shortening alternations which we mentioned above eventually get carried out. However, it is not clear how long to wait for a given string

    FIGURE 11. A systematically constructed "tree" of all the theorems of the MIU -system.
    The N th level down contains those theorems whose derivations contain exactly N steps.
    The encircled numbers tell which rule was employed. Is MU anywhere in this tree?

    to appear on this list, since theorems are listed according to the shortness of their derivations. This is not a very useful order, if you are interested in a specific string (such as MU ), and you don't even know if it has any derivation, much less how long that derivation might be.
    Now we state the proposed "theoremhood-test":

    Wait until the string in question is produced; when that happens, you know it is a theorem-and if it never happens, you know that it is not a theorem.

    This seems ridiculous, because it presupposes that we don't mind waiting around literally an infinite length of time for our answer. This gets to the crux of the matter of what should count as a "test". Of prime importance is a guarantee that we will get our answer in a finite length of time. If there is a test for theoremhood, a test which does always terminate in a finite

    amount of time, then that test is called a decision procedure for the given formal system.
    When you have a decision procedure, then you have a very concrete characterization of the nature of all theorems in the system. Offhand, it might seem that the rules and axioms of the formal system provide no less complete a characterization of the theorems of the system than a decision procedure would. The tricky word here is
    "characterization". Certainly the rules of inference and the axioms