Gödel, Escher, Bach - ein Endloses Geflochtenes Band

von n codiert ist.
    Schritt 2 ist trivial , und auch Schritt 1 ist im folgenden Sinn unkompliziert: Es kommen keine Suchaktionen mit offenem Ende in Betracht, auch keine verborgenen endlosen Schleifen. Man erinnere sich der obigen Beispiele, im MIU-System, und ersetze im Geiste die Regeln für TNT durch die von MIU und die Axiome von TNT durch die des MIU-Systems. In beiden Fällen ist der Algorithmus derselbe. Ich will ihn deutlich machen:
    Man gehe die Zeilen der Ableitung eine nach der anderen hinunter.
    Man markiere diejenigen, die Axiome sind.
    Bei jeder Zeile, die kein Axiom ist, prüfen wir, ob sie auf Grund einer Schlußregel in der angeblichen Ableitung aus früheren Zeilen folgt.
    Wenn alle Nicht-Axiome gemäß der Schlußregeln aus früheren Zeilen folgen, dann hat man eine zulässige Ableitung; sonst ist sie unrichtig.
    In jedem Stadium gibt es eine klare Anzahl von zu erledigenden Aufgaben, und ihre Anzahl läßt sich ganz leicht im voraus bestimmen.
Die Eigenschaft „Beweispaar“ ist primitiv rekursiv ...
    Warum ich die Tatsache betone, daß diese Schleifen begrenzt sind, hat seinen Grund darin — wie der Leser vielleicht schon gemerkt hat —, daß ich die Behauptung aufstellen will:
    G RUNDTATSACHE 1: Die Eigenschaft, ein Beweispaar zu sein, ist eine primitiv-rekursive zahlentheoretische Eigenschaft und kann deshalb vermittels eines BlooP-Programms getestet werden.
    Hier ist ein wichtiger Unterschied festzuhalten gegenüber der anderen, verwandten zahlentheoretischen Eigenschaft, der einer S ATZ -Zahl. Wenn man behauptet, daß n eine S ATZ -Zahl ist, behauptet man auch, daß es irgendeinen Wert von m gibt, der ein Beweispaar mit n bildet. (übrigens gelten diese Bemerkungen gleichermaßen für das TNT- wie für das MIU-System; es ist vielleicht nützlich, sich beide vor Augen zu halten, wobei das MIU-System als Prototyp dient.) Um zu prüfen, ob n eine S ATZ -Zahl ist, muß man sich auf die Suche nach allen seinen potentiellen Beweispaar-„Partnern“ m machen. Und hier kann man in eine Jagd ohne Ende geraten. Niemand kann sagen, wie weit man suchen muß, um eine Zahl zu finden, die mit m als zweitem Element ein Beweispaar mit n bildet. Das ist das ganze Problem, wenn man im gleichen System Verlängerungs- und Verkürzungsregeln hat: sie sind bis zu einem gewissen Grad nicht voraussagbar.
    An diesem Punkt kann das Beispiel der Goldbach-Variationen nützlich sein. Zu testen, ob ein Zahlenpaar (m, n) ein Schildkrötenpaar bildet, ist trivial, das heißt sowohl m wie n + m sollten prim sein. Der Test ist leicht, weil die Eigenschaft, eine Primzahl zu sein, primitiv-rekursiv ist: es gibt dafür einen voraussagbaren endlichen Test. Wollen wir jedoch wissen, ob n die Schildkröten-Eigenschaft hat, dann fragen wir: „Gibt es irgendeine Zahl m, die ein Schildkrötenpaar mit n als zweitem Element bildet?“ — und das führt uns wieder hinaus in das wilde, MU-schleifige Unbekannte.
... und deshalb in TNT repräsentiert
    Der Schlüsselbegriff an diesem Punkt ist also die oben gegebene Grundtatsache 1, denn aus ihr können wir folgern:
    G RUNDTATSACHE 2: Die Eigenschaft, Beweispaare zu bilden, läßt sich mit BlooP testen, und sie ist deshalb in TNT durch eine Formel repräsentiert, die zwei freie Variablen besitzt.
    Auch hier geben wir uns keine besondere Mühe, um zu bestimmen, auf welches System diese Beweispaare sich beziehen; im Grunde ist es unwichtig, da beide Grundtatsachen in jedem formalen System Gültigkeit besitzen. Das liegt in der Natur formaler Systeme: es ist immer möglich, auf voraussagbar endliche Art und Weise zu bestimmen, ob eine gegebene Zeilenfolge einen Beweis bildet oder nicht. Und das läßt sich auf die entsprechenden arithmetischen Begriffe übertragen.
Die Leistungsfähigkeit von Beweispaaren
    Um der Anschaulichkeit willen nehmen wir an, daß wir es mit dem MIU-System zu tun haben. Der Leser wird sich an die Kette erinnern, die wir „M UMON “ nannten und deren Interpretation auf einer gewissen Stufe die Aussage war: „ MU ist ein S ATZ des MIU-Systems.“ Wir können zeigen, wie M UMON in TNT ausgedrückt würde, also vermittels der Formel, die die Aussage des MIU-Beweispaars repräsentiert. Kürzen wir diese Formel, deren Existenz unsere Grundtatsache 2 gewährleistet, so ab:
    MIU-Beweispaar { a,a '}
    Da es sich um eine Eigenschaft von zwei Zahlen handelt, ist sie durch eine Formel mit zwei freien Variablen darstellbar. (Anmerkung: In diesem Kapitel werden wir durchwegs