Gentzenscher Hauptsatz
aus Wikipedia, der freien Enzyklopädie
Der Gentzensche Hauptsatz (Auch: Schnittsatz, cut-elimination theorem) besagt, dass die Transitivität in speziellen Logikkalkülen zulässig ist.
Inhaltsverzeichnis |
[Bearbeiten] Einleitung
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. Alle Herleitungen durch Kalkülregeln in Gentzentypkalkülen, die die transitive Schnittregel verwenden, können so umformuliert werden, dass sie die Schnittregel nicht verwenden. Die Schnittregel (engl. cut oder cut-rule) ist der modus ponens auf metalogischer Stufe und lautet so:
Bei einer Herleitbarkeit der Formel A und einer Herleitbarkeit der Formel B mit Hilfe von A gehe über zu Formel B ist (auch allein) herleitbar.
Der Hauptsatz zeigt also die Berechtigung (Redundanz) dieser Übergangsregel, wenn die übrigen Kalkülregeln vorausgesetzt werden.
(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.)
[Bearbeiten] 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 in 
, so kann man die Herleitung von a in 
statt a selbst benutzen. Andernfalls kann a überall wegfallen.
- 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 Δ − M bezeichnet die Formelfolge, die entsteht, wenn man in Δ jedes vorkommende M streicht (Schreibweise hier mit Doppelpfeil für die Herleitbarkeit).
[Bearbeiten] 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 
. 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).
[Bearbeiten] Bedeutung und Anwendungen
Die Entfernung von Schnitten (engl.: cut-elimination) ist nicht nur eine Möglichkeit die Schnittregel als gültig zu beweisen, sondern umgedreht ein sehr nützliches mathematisch-logisches Werkzeug, beispielsweise beim Beweis des Interpolation-Theorems von Craig und Schütte. Die Möglichkeit Beweise durchzuführen, die auf Resolution beruhen, ist sehr mächtig (Maschinengestütztes Beweisen). Der Lauf eines Prolog-Programms (d.h. das, was passiert, während das Prolog-Programm läuft) lässt sich als schnittfreie Kalkül-Herleitung interpretieren.
Führt man allerdings in Gentzentypkalkülen Beweise durch, die den Schnitt vermeiden (analytic proofs), so sind diese Beweise 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 Lebenszeit des Universums dauern 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.
[Bearbeiten] Literatur
- Gerhard Gentzen: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39] (1934).
- Nachdruck in: Karel Berka, Lothar Kreiser: 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
- Sakharov, Alex. "Cut Elimination Theorem." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. [1]
- Rüdiger Inhetveen: Logik. Eine dialog-orientierte Einführung, Leipzig 2003 ISBN 3-937219-02-1
