Der Gentzensche Hauptsatz (Auch: Schnittsatz, cut-elimination theorem) besagt, dass die Transitivität (der Schnitt) in speziellen Logikkalkülen zulässig ist: Alle Herleitungen durch Kalkülregeln in Gentzentypkalkülen, die die Schnittregel verwenden, können so umformuliert werden, dass sie die Schnittregel nicht verwenden.
Entstehung
Der Hauptsatz ist ein metalogischer Satz und wurde von Gerhard Gentzen 1934 aufgestellt und bewiesen. Er ist ein wichtiger Satz in der Logik und Informatik.
Die ursprüngliche Form des Hauptsatzes lautet so: Jede LJ- bzw. LK-Herleitung läßt sich in eine LJ- bzw. LK-Herleitung mit gleicher Endsequenz umwandeln, in welcher die als "Schnitt" bezeichnete Schlussfigur nicht vorkommt.
Schnittregel
Die Schnittregel (engl. cut oder cut-rule) ist der modus ponens auf metalogischer Stufe und lautet so:
Ist also die Formel (oder Aussage) A herleitbar, ist außerdem mit Hilfe von A die Formel B herleitbar, so ist B herleitbar: A kann man wegschneiden. (Die griechischen Buchstaben und stehen für Listen von Formeln, die im Voraus als herleitbar angesehen werden (Hornklauseln, Sequenzen). Für die Herleitbarkeit wird hier der Doppelstrich || der Abschließbarkeit von Dialogstellungen benutzt.)
Beweisskizze
Die Beweise für diesen Hauptsatz liegen inzwischen in einfacher Form vor (Inhetveen 2003, S.197; Heindorf 1994, S.105; Lorenzen 2000, S.81).
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 ):
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 mit den Kalkülregeln für dieses Zeichen zu der Schnittregel in der Form An+1 übergehen darf.
Von
prüfe pro Logikzeichen, ob:
gültig ist. Bei den Junktoren ist der Beweis relativ einfach, aber man hat eine Menge von Fallunterscheidungen. 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:
M heißt Mischformel und bezeichnet die Formelfolge, die entsteht, wenn man in jedes vorkommende M streicht (Schreibweise hier mit Doppelpfeil für die Herleitbarkeit).
Widerspruchsfreiheit
Die Kalküle, 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 A. Die Negation ist dieser Spezialfall der Subjunktion.
Setzt man nun (für B) f in die Schnittregel ein:
so folgt aus der Herleitbarkeit von A und der (gerade erwähnten) von 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. Alle anderen werden ja durch die Schnittregel eliminiert. In einem inkonsistenten Kalkül lässt sich die leere Sequenz: " || " ableiten. Da sie aber keine Teilformeln hat, kann sie nicht entstanden sein.
Widerspruchsfreiheitsbeweise der Mathematik werden durchgeführt, indem man die transfinite Induktion (Gerhard Gentzen) oder die unendliche Induktion, also die -Regel (Kurt Schütte, Paul Lorenzen), in die Beweise dieses Hauptsatzes einbindet (vollständiger Halbformalismus).
Bedeutung und Anwendungen
Die Schnittvermeidung (engl.: cut-elimination) ist ein sehr nützliches Werkzeug, beispielsweise beim Beweis von Interpolationssätzen. Die Möglichkeit, Beweise durchzuführen die auf Resolution beruhen, ist sehr mächtig. Das Verfahren lässt sich auch auf die Informatik übertragen. Ein Lauf eines Prolog-Programms beispielsweise (d.h. das, was passiert, während das Prolog-Programm läuft) lässt sich als Herleitung in einem Gentzentypkalkül interpretieren.
Führt man in Gentzentypkalkülen Beweise durch, die den Schnitt vermeiden (analytic proofs), so sind diese Beweise allerdings in der Regel länger als bei Verwendung der Schnittregel. In dem Essay "Don't Eliminate Cut!" zeigt der Mathematiker und Logiker George Boolos, dass es eine Herleitung gibt, die mit Schnitt etwa eine Seite beträgt ohne Benutzung des Schnitts aber die Größe des Universums ausmachen würde.
Durch die Anwendung der Schnittregel lassen sich modallogische Aussagen rechtfertigen, wenn die entsprechenden logischen Aussagen wahr sind. Das in der Modallogik immer zu unterstellende Wissen kann in dem Fall weggeschnitten werden. Der Gentzensche Hauptsatz dient also auch zur Fundierung der Modallogik, weil man so modallogische Wahrheit definieren kann.
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
- Online-Version der Uni Göttingen: Teil 1 und Teil 2
- 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
- Kuno Lorenz, P. Lorenzen: Dialogische Logik, Darmstadt 1978 - (Enthält zum ersten Mal einen Beweis auf dialogisch-spieltheoretischer Basis.)
- Paul Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Zürich 1987, Stuttgart 2000, ISBN 3-476-01784-2
- 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
- George Boolos: Don't eliminate cut in: Journal of Philosophical Logic 13 (1984), pp. 373-378.
- 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
- Rüdiger Inhetveen: Logik. Eine dialog-orientierte Einführung, Leipzig 2003 ISBN 3-937219-02-1