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

von „strengem“ TNT Gebrauch machen — man unterscheide also sorgfältig zwischen den Variablen a , a' , a'' usw.)
    Um zu behaupten: „ MU ist ein S ATZ des MIU-Systems“, müßten wir die isomorphe Aussage machen: „30 ist eine S ATZ -Zahl des MIU-Systems“, und sie dann in die TNT-Notation übersetzen. Mit Hilfe unserer Abkürzung ist das einfach (man erinnere sich an die Tatsache — Kapitel VIII —, daß wir, um die Substitution jedes a' durch ein Zahlzeichen anzugeben, wir dieses Zahlzeichen niederschreiben, und darauf „/ a' “ folgen lassen):
    ∃a:MIU-Beweispaar { a , SSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0 / a '}
    Man zähle die „ S “ ; es sind dreißig. Man beachte, daß das kein offener Satz von TNT ist, weil eine freie Variable quantifiziert und die andere durch ein Zahlzeichen ersetzt wurde. Übrigens ist hier etwas ganz Schlaues passiert. Grundtatsache 2 verschafft uns die Möglichkeit, von Beweispaaren zu sprechen; wir haben uns klargemacht, wie man außerdem über S ATZ -Zahlen sprechen kann: Man fügt einfach vorn einen Existenzquantor an. Eine eher wörtliche Übersetzung dieser Kette wäre: „Es gibt eine Zahl a, die ein MIU-Beweispaar mit 30 als zweitem Element bildet.“
    Angenommen, wir wollten etwas Paralleles im Hinblick auf TNT tun — sagen wir, die Aussage „ 0 = 0 ist ein S ATZ von TNT“ ausdrücken. Wir können die Formel, deren Existenz uns Grundtatsache 2 garantiert, auf analoge Weise abkürzen (wieder mit zwei freien Variablen):
    TNT-BEWEISPAAR { a , a '}
    (Die Interpretation dieser abgekürzten TNT-Formel ist „Natürliche Zahlen a und a ' bilden ein TNT-Beweispaar“.) Der nächste Schritt ist der, daß wir unsere Aussage in die Zahlentheorie übersetzen, wobei wir dem obigen M UMON -Modell folgen. Aus der Aussage wird: „Es gibt eine Zahl a , die mit 666,111,666 als zweitem Element ein Beweispaar bildet.“ Die TNT-Formel, die das ausdrückt, lautet:
∃a:TNT-BEWEISPAAR { a , SSSSS ... SSSSS0 / a '}
∃a:TNT-BEWEISPAAR { a
∃a:TNT-BEWEISPAAR { a , SS viele, viele S !
∃a:TNT-BEWEISPAAR { a (nämlich 666,111,666)
    — eine geschlossene Aussage in TNT. (Nennen wir sie aus Gründen, die gleich klar werden, „J ŌSHŪ “.) Man sieht also, daß es eine Methode gibt, nicht nur über die primitiv-rekursiven Begriffe von TNT-Beweispaaren zu sprechen, sondern auch über den verwandten, doch kniffligeren Begriff der TNT-S ATZ -Zahlen.
    Zur Prüfung unseres Verständnisses dieser Ideen möge der Leser herausfinden, wie die folgenden Aussagen von Meta-TNT in TNT zu übersetzen wären:
1)
0 = 0 ist kein S ATZ von TNT.
2)
~ 0 = 0 ist ein S ATZ von TNT.
3)
~ 0 = 0 ist kein S ATZ von TNT.
    Wie unterscheiden sich die Lösungen von den obigen Beispielen und voneinander? Hier noch ein paar Übersetzungsübungen:
4)
J ŌSHŪ ist ein S ATZ von TNT. (Man nenne die TNT-Kette, die das ausdrückt „M ETA -J ŌSHŪ “.)
5)
M ETA -J ŌSHŪ ist ein S ATZ von TNT. (Man nenne die TNT-Kette, die das ausdrückt „M ETA -M ETA -J ŌSHŪ “.)
6)
M ETA -M ETA -J ŌSHŪ ist ein S ATZ von TNT.
7)
M ETA -M ETA -M ETA -J ŌSHŪ ist ein S ATZ von TNT.
    (usw., usw.)
    Beispiel 5 zeigt, daß Aussagen von Meta-Meta-TNT in die TNT-Notation übersetzt werden können! Beispiel 6 leistet dasselbe für Meta-Meta-Meta-TNT usw.
    Wichtig ist es, sich an den Unterschied zu erinnern, der zwischen dem Ausdrücken einer Eigenschaft und der Repräsentierung einer solchen besteht. Die Eigenschaft, eine TNT-S ATZ -Zahl zu sein, wird zum Beispiel ausgedrückt durch die Formel
    ∃a:TNT-BEWEISPAAR { a,a '}
    Übersetzung: „ a ' ist eine TNT-S ATZ -Zahl.“ Wir haben aber keine Garantie, daß diese Formel den Begriff repräsentiert, weil wir keine Garantie haben, daß diese Eigenschaft primitiv-rekursiv ist — wir hegen sogar den mehr als leisen Verdacht, daß sie es nicht ist. (Dieser Verdacht ist wohlbegründet. Die Eigenschaft, eine TNT-S ATZ -Zahl zu sein, ist nicht primitiv-rekursiv, und keine TNT-Formel kann die Eigenschaft repräsentieren!)
    Im Gegensatz dazu ist die Eigenschaft, ein Beweispaar zu sein, kraft seiner primitiven Rekursivität durch die bereits angegebene Formel sowohl ausdrückbar als repräsentierbar.
Substitution führt zu der zweiten Idee
    Die vorhergehende Diskussion brachte uns bis zu dem Punkt, an dem wir sahen, wie TNT „introspektiv“ prüfen kann, ob ein S ATZ ein TNT-S ATZ ist. Das ist das Wesentliche des ersten Teils des Beweises. Wir wollen nunmehr zum zweiten Hauptgedanken des Beweises