Gentzenscher Hauptsatz

Der Gentzensche Hauptsatz (Auch: Schnittsatz, cut-elimination theorem) besagt, dass die Transitivität in Logikkalkülen zulässig ist. Das Wegschneiden von transitiven Zwischengliedern (auch in Suchbäumen) ändert nichts an den Herleitungen.

In der Regellogik geht es um folgenden Zusammenhang:

Alle Beweise durch Kalkülregeln in Gentzentypkalkülen, die die Schnittregel verwenden, können so umformuliert werden, dass sie die Schnittregel nicht verwenden. Unter Gentzentypkalkülen versteht man die Sequenzenkalküle, die Systeme des natürlichen Schließens, die Bethschen Tableaux und die Dialogische Logik.

Die Schnittregel (engl. cut oder cut-rule) ist der modus ponens auf metalogischer Stufe und lautet so:

$\qquad {\frac {\Gamma \|A\qquad A,\Delta \|B}{\Gamma ,\Delta \|B}}$

Die griechischen Buchstaben $\Gamma$ und $\Delta$ stehen für Listen von Formeln, die im Voraus als herleitbar angesehen werden (Hornklauseln, Sequenzen). Für die Herleitbarkeit wird der Doppelstrich || der Abschließbarkeit von Dialogstellungen benutzt.

Ist die Formel (oder Aussage) A herleitbar, - ist außerdem mit Hilfe von A die Formel B herleitbar, - so ist B (auch allein) herleitbar: A kann man also wegschneiden.

Entstehung

Der Hauptsatz ist ein metalogischer Satz und wurde zuerst von dem Beweistheoretiker Gerhard Gentzen 1934 aufgestellt und bewiesen. Er ist ein wichtiger Satz in der Logik und Informatik.

Beweisskizze

Die Beweise für diesen Hauptsatz liegen inzwischen in einfacher Form vor (Paul Lorenzen 1987/2000 S. 81-83, Lutz Heindorf 1994, S. 105 ff.)

Die Beweisskizze ist folgende:

Beweis durch Vollständige Induktion über die Anzahl der Teilformeln in A (Teilformelinduktion):

Induktionsanfang (a ist eine Prim- bzw Atomformel also nicht zusammengesetzt n=1 ):

$\qquad {\frac {\Gamma \|a\qquad a,\Delta \|\ B}{\Gamma ,\Delta \|\ B}}$

Begründung für die Zulässigkeit: Benutzt man a für die Herleitung von B, so kann man die Herleitung von a für die Herleitung von B statt a selbst benutzen. Andernfalls kann a überall wegfallen. Also ist B ohne a herleitbar, die Konklusion berechtigt.

Beweisidee für den Induktionsschritt (n zu n+1):

Nun weist man bei der Schnittregel in der Form An (aus n Teilformeln zusammengesetzte Formel) für jedes logische Zeichen nach, dass man bei den Kalkülregeln für dieses Zeichen zu der Schnittregel in der Form An+1 übergehen darf.

Von

$\qquad {\frac {\Gamma \|An\qquad An,\Delta \|\ B}{\Gamma ,\Delta \|\ B}}$

prüfe pro Logikzeichen, ob:

$\qquad {\frac {\Gamma \|An+1\qquad An+1,\Delta \|\ B}{\Gamma ,\Delta \|\ B}}$

gültig ist.

Bei den Quantoren wird im dialogischen Beweis über die Anzahl der Entwicklungsschritte indiziert. Manche Beweise (siehe Gentzen und Heindorf) benutzen zusätzlich zur Schnittregel auch die so genannte Mischregel (Mix), die der Schnittregel ähnlich ist:

$\qquad {\frac {\Gamma \Rightarrow M\qquad \Delta \Rightarrow \ B}{\Gamma ,\Delta -M\Rightarrow \ B}}$

M heißt Mischformel und $\Delta -M$ bezeichnet die Formelfolge, die entsteht, wenn man in $\Delta$ jedes vorkommende M streicht (Schreibweise hier mit Doppelpfeil für die Herleitbarkeit).

Schnittfreiheit und Gültigkeit der Schnittregel

Der Hauptsatz ist ein sehr mächtiges Instrument der modernen Beweistheorie mit Auswirkungen auf die Informatik, Mathematik und Logik. Er ist auf zwei Weisen interpretierbar:

1. Er zeigt die Schnittvermeidung (cut-elimination) auf, indem er zeigt, wie die Herleitungen und Programme so umformuliert werden, dass keine transitiven Umwege mehr da sind.
2. Er weist die Widerspruchsfreiheit der Systeme nach.

Dabei ist zu beachten, dass die Schnittregel nicht zu den Kalkülregeln dazugehören muss, wenn sie in Bezug auf die übrigen Regeln zulässig (gültig, redundant, engl.: admissible) ist.

Vermeidung der Schnittregel beim Programmieren

Betrachtet man beim Automatischen Problemlösen und in der Constraintprogrammierung das Verfolgen eines Suchbaums als Beweis in einem Kalkül, so entspricht die Brute-Force-Methode einem Beweis, der noch Umwege über den Schnittknoten A geht. Diese Umwege werden (etwa durch einen Alpha-Beta-Cut) weggeschnitten. In der Programmiersprache Prolog wird dies ausgenutzt. Das backtracking vermeidet diese Umwege.

Schnittfreiheit bedeutet in der Programmierung, dass Umwege über einen unnötigen Knoten eines Suchbaums vermieden werden, so dass ein Schnitt nicht nötig ist. Dies ist ein wichtiges Programmierziel. In schnittfreien Suchbäumen wird die Beweissuche (proof search) wesentlich einfacher. Es entstehen so Graphen ohne Mehrfachkanten.

Widerspruchsfreiheit

Die Kalkülsysteme für die der Hauptsatz gilt sind widerspruchsfrei.

Ein Gedankengang der Widerspruchsfreiheit ist folgender: Sei f (lies: falsch oder falsum) per definitionem nicht herleitbar. Dann ist A || f nichts anders als die Herleitbarkeit von $\neg$A. Die Negation ist dieser Spezialfall der Subjunktion.

Setzt man nun (für B) f in die Schnittregel ein:

$\qquad {\frac {\Gamma \|A\qquad \Gamma ,A\|\ f}{\Gamma \|\ f}}$

so folgt aus der Herleitbarkeit von A und der (gerade erwähnten) von $\neg$A (beides zusammen ist ein Widerspruch), die Herleitbarkeit vom unherleitbaren f, was nicht sein kann. - Die Herleitbarkeit eines Widerspruchs in den Prämissen wird also metalogisch ad absurdum geführt.

Eine andere Widerspruchsfreiheitsüberlegung ist folgende: Aus dem Hauptsatz ergibt sich, dass in einer Herleitung nur Teilformeln derjenigen Formeln auftreten, die in der hergeleiteten Endsequenz vorkommen. In einem inkonsistenten Kalkül läßt sich die leere Sequenz: || ableiten. Zur ihr gibt es aber keine Teilformeln.

Widerspruchsfreiheitsbeweise der Mathematik werden durchgeführt, indem man die transfinite Induktion (Gerhard Gentzen) oder die unendliche Induktion, also die $\omega$-Regel (Kurt Schütte, Paul Lorenzen) in die Beweise dieses Hauptsatzes einbindet (vollständiger Halbformalismus).

Der so genannte verschärfte Hauptsatz (sharpened Hauptsatz) ist dem Satz von Herbrand (Herbrand's theorem) ähnlich. Dabei geht es um die Rolle der Quantoren in einem Beweis.

Literatur

• Gerhard Gentzen: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39 (1934). Nachdruck in: Karel Berka, Lothar Kreier: Logik-Texte, Berlin (Ost) 1986
• S. C. Kleene: Introduction to Metamathematics, Amsterdam Groningen 1952
• Paul Lorenzen: Metamathematik, Mannheim 1962
• Gerhard Gentzen (hrsg.M. E. Szabo): The Collected Papers of Gerhard Gentzen, Amsterdam 1969
• Paul Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Zürich 1987, Stuttgart 2000, ISBN 3-476-01784-2
• K. Lorenz, P. Lorenzen: Dialogische Logik, Darmstadt 1978
• Kurt Schütte: Beweistheorie, Berlin Göttingen Heidelberg 1960
• A. S. Troelstra, H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. ISBN 0521779111
• Gerrit Haas: Konstruktive Einführung in die formale Logik 1984 ISBN 3411016280
• Lutz Heindorf: Elementare Beweistheorie, 1994 ISBN 3411171618
• Eckart Menzler-Trott: Gentzens Problem. Mathematische Logik im nationalsozialistischen Deutschland. Birkhäuser Verlag, Basel 2001, ISBN 3764365749
• Peter Schroeder-Heister: Cut-elimination in logics with definitional reflection. Nonclassical Logics and Information Processing, 146–171, 1990. In D. Pearce, H. Wansing (Herausgeber): Nonclassical Logics and Information Processing. International Workshop, Berlin, November 9–10 1990, Proceedings. Springer Lecture Notes in Artificial Intelligence 619, Berlin/Heidelberg/New York 1992, ISBN 3-540-55745-8.
• Jean-Yves Girard: Proofs and Types Cambridge University Press 1989; reprint web 2003