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

zweite nicht. Die Regel macht das Additionskriterium zu einer vererbbaren Eigenschaft der S ÄTZE : Jeder S ATZ gibt die Eigenschaft an seinen Nachfolger weiter. Das zeigt, warum das Additionskriterium korrekt ist.
    Es gibt übrigens eine Tatsache im pg-System, die uns ermöglicht, mit Zuversicht zu sagen, daß es ein Entscheidungsverfahren besitzt, sogar noch bevor man das Additionskriterium findet. Diese Tatsache ist die, daß das pg-System nicht durch die einander widerstrebenden Strömungen der Verlängerungs- und Verkürzungs-Regeln kompliziert wird; es besitzt nur Verlängerungs-Regeln. Jedes formale System, das uns sagt, wie man längere aus kürzeren S ÄTZEN machen kann, niemals aber das Gegenteil, muß für seine S ÄTZE ein Entscheidungsverfahren besitzen. Nehmen wir an, man lege uns eine Kette vor. Prüfen wir zuerst, ob es sich um ein Axiom handelt oder nicht. (Ich nehme an, daß es ein Entscheidungsverfahren dafür gibt, ob es sich um Axiome handelt; sonst ist alles hoffnungslos.) Wenn es sich um ein Axiom handelt, dann ist es definitionsgemäß ein S ATZ , und der Test ist zu Ende. Nehmen wir aber an, es handle sich nicht um ein Axiom. Um ein S ATZ zu sein, muß es gemäß einer der Regeln von einer kürzeren Kette abstammen. Indem wir nacheinander die verschiedenen Regeln prüfen, können wir nicht nur die Regeln identifizieren, die möglicherweise diese Kette hervorbringen konnten, sondern auch feststellen, welche kürzeren Ketten ihre Vorläufer im „Stammbaum“ sein könnten. Auf diese Weise „reduziert“ man das Problem auf die Feststellung, ob eine von irgendwelchen neuen, aber kürzeren Ketten einen S ATZ darstellt. Jede von ihnen kann ihrerseits demselben Test unterworfen werden. Das schlimmste, was geschehen kann, ist eine Flut von immer mehr, aber immer kürzeren Ketten, die getestet werden müssen. Während wir auf diese Weise unseren Weg langsam nach rückwärts gehen, müssen wir der Quelle aller S ÄTZE — den Axiomen-Schemata — näherkommen. Aber die Ketten können nicht ad infinitum kürzer und kürzer werden; deshalb werden wir schließlich finden, daß eine unserer kurzen Ketten ein Axiom ist, oder wir kommen zu einem Punkt, an dem es nicht mehr weiter geht, weil keine unserer kurzen Ketten ein Axiom ist, und keine noch weiter verkürzt werden kann, wenn man die eine oder andere Regel rückläufig anwendet. Das zeigt, daß formale Systeme, die lediglich Verlängerungs-Regeln enthalten, nicht übermäßig interessant sind; erst das Zusammenspiel von Verlängerungs- und Verkürzungs-Regeln verleiht formalen Systemen eine gewisse Faszination.
Bottom-up — Top-down
    Die obige Methode könnte man als top-down-Entscheidungsverfahren („von oben nach unten“) bezeichnen, im Gegensatz zu dem bottom-up-Verfahren („von unten nach oben“), das ich jetzt angeben werde. Es erinnert stark an die systematische S ATZ erzeugende Methode des Dämonen im MIU-System, wird aber durch das Vorhandensein eines Axiomenschemas kompliziert. Wir bilden einen „Eimer“, in den wir die S ÄTZE so werfen, wie sie anfallen. Das geht so vor sich:
1a)
Wirf das einfachste Axiom ( −p−g−− ) in den Eimer.
1b)
Wende die Schlußregel auf den S ATZ im Eimer an, und tue das Ergebnis in den Eimer.
2a)
Wirf das zweiteinfachste Axiom in den Eimer.
2b)
Wende die Regel auf jede Kette im Eimer an, und wirf alle Ergebnisse in den Eimer.
3a)
Wirf das dritteinfachste Axiom in den Eimer.
3b)
Wende die Regel auf jede Kette im Eimer an, und wirf alle Ergebnisse in den Eimer.
usw. usw.
    Eine kurze Überlegung zeigt, warum wir auf diese Weise unfehlbar jeden S ATZ des pg-Systems erhalten werden. Außerdem wird der Eimer mit der Zeit mit immer längeren S ÄTZEN gefüllt. Das ist wiederum eine Folge davon, daß es keine Verkürzungs-Regel gibt. Wenn wir also eine bestimmte Kette besitzen, z. B. −−p−−−g−−−−− , von der wir herausfinden wollen, ob sie ein S ATZ ist, folgen wir einfach den numerierten Schritten und halten dabei immer Ausschau nach der in Frage stehenden Kette. Wenn sie auftaucht — S ATZ ! Wenn an einem gewissen Punkt alles, was in den Eimer geworfen wird, länger ist als die Kette, vergessen Sie es — sie ist kein S ATZ ! Dieses Entscheidungsverfahren verläuft „bottom-up“, weil es sich von den Grundvoraussetzungen, d. h. den Axiomen, nach oben bewegt. Das vorhergehende Verfahren verläuft „top-down“, weil es genau umgekehrt vorgeht: Es geht nach unten zu den