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

Carroll-Dialog zurückzukehren, und die verschiedenen Stadien der Debatte in unsere Notation zu codieren, wobei man mit dem ursprünglichen Zankapfel beginnt:
    Achilles: Wenn Sie << A ∧ B >⊃ Z > haben und außerdem < A ∧ B >, dann haben Sie sicher Z .
    Schildkröte: Oh, Sie meinen: <<<< A ∧ B ⊃ Z >∧< A ∧ B >>⊃ Z >, nicht wahr?
    (Hinweis: Was immer Achilles als Schlußregel auffaßt, flacht die Schildkröte sofort lediglich zu einer Kette des Systems ab. Wenn man nur die Buchstaben A , B und Z verwendet, erhält man ein rekursives Muster von immer längeren Ketten.)
Abkürzungen und abgeleitete Regeln
    Wenn man in der Aussagenlogik Ableitungen vornimmt, erfindet man bald verschiedene Arten von Abkürzungen, die streng genommen nicht Teile des Systems sind.
    Wenn zum Beispiel die Kette < Q ∨~ Q > benötigt würde, und < P ∨~ P > schon früher abgeleitet worden ist, würden viele so vorgehen, als wäre < Q ∨~ Q > abgeleitet, da sie wissen, daß ihre Ableitung eine genaue Parallele zu der von < P ∨~ P > bildet. Der abgeleitete S ATZ wird als „S ATZ -Schema“, als Gußform für andere S ÄTZE behandelt. Das erweist sich als ein völlig gerechtfertigtes Vorgehen, da es immer zu neuen S ÄTZEN führt, aber es ist keine Regel der Aussagenlogik, wie wir sie dargelegt haben. Vielmehr ist es eine abgeleitete Regel. Es ist ein Teil des Wissens, das wir über das System besitzen. Daß Anwendungen dieser Regel nur richtige S ÄTZE ergeben, bedarf natürlich des Beweises — aber ein solcher Beweis ist nicht wie eine Ableitung innerhalb des Systems, es ist ein Beweis im gewöhnlichen, anschaulichen Sinn — eine Kette von folgerichtigen Denkschritten, ausgeführt im I-Modus. Die Theorie über die Aussagenlogik ist eine „Metatheorie“, und die Ergebnisse in ihr kann man „Meta-S ÄTZE “ nennen: Sätze über S ÄTZE . (Man beachte nebenbei die komische Großschreibung im Ausdruck „Sätze über S ÄTZE “ — eine Folge unserer Vereinbarung: Meta-S ÄTZE sind Sätze (bewiesene Ergebnisse), die S ÄTZE (ableitbare Ketten) betreffen.)
    In der Aussagenlogik könnte man zahlreiche andere Meta-S ÄTZE oder abgeleitete Schlußregeln entdecken. Zum Beispiel gibt es eine zweite De Morgans Regel:
    <~ x  ∨~ y > und ~< x  ∧  y > sind austauschbar.
    Wäre das eine Regel des Systems, würde es viele Ableitungen erheblich beschleunigen. Genügt es aber nicht, zu beweisen, daß diese Regel korrekt ist? Können wir sie von nun an nicht einfach wie ein Schlußregel verwenden?
    Es liegt kein Grund vor, die Korrektheit dieser bestimmten abgeleiteten Regel anzuzweifeln. Wenn man aber einmal damit anfängt, bei der Arbeit mit der Aussagenlogik abgeleitete Regeln zuzulassen, hat man die Formalität des Systems verloren, da abgeleitete Regeln informal — außerhalb des Systems — abgeleitet werden. Nun hat man formale Systeme vorgeschlagen als eine Methode, jeden Schritt eines Beweises innerhalb eines starren Rahmens explizit aufzuzeigen, so daß jeder Mathematiker die Arbeit eines anderen mechanisch prüfen könnte. Wenn man aber bereit ist, bei der geringsten Gelegenheit diesen Rahmen zu verlassen, hätte man ihn genausogut gar nicht erst errichten brauchen. Deshalb hat die Verwendung solcher Abkürzungen ihre Nachteile.
Formalisierung höherer Ebenen
    Doch gibt es einen Ausweg. Warum nicht auch die Meta-Theorie formalisieren? Dann wären abgeleitete Regeln (Meta-S ÄTZE ) S ÄTZE eines größeren formalen Systems, und es wäre legitim, nach Abkürzungen Ausschau zu halten, und sie als S ÄTZE abzuleiten d. h.: S ÄTZE der formalisierten Meta-Theorie — die dann dazu verwendet werden könnten, die Ableitungen von S ÄTZEN der Aussagenlogik zu beschleunigen. Das ist ein interessanter Gedanke, aber sobald man ihn vorschlägt, springt man auch schon weiter und denkt an Meta-Meta-Theorien, usw. Es ist klar, daß, soviel Ebenen man auch formalisiert haben mag, irgend jemand schließlich einmal auf der obersten Ebene Abkürzungen vornehmen will.
    Man könnte sogar zu bedenken geben, daß eine Theorie des folgerichtigen Denkens, sorgfältig ausgearbeitet, mit ihrer eigenen Meta-Theorie identisch sein könnte. Dann könnte es sein, daß alle Ebenen in eine Zusammenfallen, und über das System zu denken wäre einfach eine Methode, in ihm zu denken. So einfach geht das aber nicht! Auch wenn das System „über sich selbst denken“ kann, ist es immer noch nicht außerhalb seiner selbst. Wer sich außerhalb des Systems