Gentzenscher Hauptsatz

Der Gentzensche Hauptsatz oder Schnittsatz ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in Gentzentypkalkülen zulässig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies.

Die Schnittregel

Die Schnittregel ist der modus ponens auf metalogischer Stufe:

Angenommen, die Sequenzen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma\vdash A} und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A, \Delta\vdash B} sind herleitbar. Die Schnittregel besagt, dass man dann zu der Sequenz Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma, \Delta\vdash B} übergehen kann, d. h. die Formel $B$ ist dann auch ohne $A$ herleitbar.

Die griechischen Buchstaben Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma} und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta} stehen dabei für Listen von Formeln, die bereits hergeleitet wurden. Für die Herleitbarkeit wird hier das Zeichen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash } benutzt.

Beweisskizze

Beweise für diesen Hauptsatz liegen inzwischen in einfacher Form vor. Die Grundidee ist, Herleitungen, in denen die Schnittregel verwendet wird, so aufzulösen (englisch: cut elimination), dass sie nicht mehr verwendet wird.

Dazu führt man eine vollständige Induktion über die Anzahl der Teilformeln in der Schnittformel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} durch (Teilformelinduktion).

Induktionsanfang (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n=1} ): Wenn $A$ nur eine Teilformel besitzt, also nicht zusammengesetzt ist, muss Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} eine Prim- bzw. Atomformel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a} sein:

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \frac{\Gamma\vdash a\qquad a, \Delta\vdash\ B}{\Gamma, \Delta\vdash\ B}} .

Im einfachsten Fall wird Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a} in der Herleitung Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a,\Delta\vdash B} nicht verwendet. Dann ist diese Herleitung auch ohne Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a} gültig, d. h. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta\vdash B} . Das bedeutet aber, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B} ohne die Schnittregel hergeleitet werden kann.

Wenn hingegen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a} in der Herleitung Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a,\Delta\vdash B} vorkommt, so kann man darin $a$ durch die Herleitung Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma\vdash a} ersetzen. Auch in diesem Fall gibt es also eine Möglichkeit, Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B} ohne die Schnittregel herzuleiten.

Induktionsschritt (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n} zu Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle n+1} ): Die Induktionsannahme besagt, dass die Schnittregel für die Formeln Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} gültig ist, die n Teilformeln haben:

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \frac{\Gamma\vdash A_n\qquad A_n, \Delta\vdash\ B}{\Gamma, \Delta\vdash\ B}} .

Nun wird eine Fallunterscheidung in Bezug auf das in:

${\frac {\Gamma \vdash A_{n+1}\qquad A_{n+1},\Delta \vdash \ B}{\Gamma ,\Delta \vdash \ B}}$

neu hinzukommende Logikzeichen durchgeführt, die Schnittregel wird also jeweils durch die Kalkülregeln für dieses Zeichen ersetzt.

Bei den Junktoren ist dieser Beweisteil trotz der vielen Fallunterscheidungen relativ einfach. Bei den Quantoren wird im dialogischen Beweis über die Anzahl der Entwicklungsschritte induziert.

Die (langen) nicht-dialogischen Beweise benutzen zur technischen Vereinfachung der Beweisführung zusätzlich die aus der Schnittregel beweisbare sogenannte Mischregel (Mix):

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \frac{\Gamma\vdash M\qquad \Delta\vdash\ B}{\Gamma, (\Delta - M) \vdash B}} .

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle M} heißt Mischformel und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta - M} bezeichnet die Formelfolge, die entsteht, wenn man in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Delta} jedes vorkommende Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle M} streicht.

Widerspruchsfreiheit

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

Ein Gedankengang für den Beweis der Widerspruchsfreiheit ist folgender: Sei Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bot} (lies: falsch oder falsum) per definitionem nicht herleitbar. Dann ist Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A \vdash \bot} nichts anderes als die Herleitbarkeit von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \neg A.} Die Negation ist dieser Spezialfall der Subjunktion.

Setzt man nun für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B} in die Schnittregel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bot} ein:

Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \frac{\Gamma\vdash A\qquad \Gamma, A\vdash\ \bot}{\Gamma\vdash\ \bot}}

so folgt aus der Herleitbarkeit von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} und der (gerade erwähnten) von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \neg } Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} (beides zusammen ist ein Widerspruch in den Prämissen) die Herleitbarkeit vom unherleitbaren Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bot} , was nicht sein kann. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma\vdash\ \bot} wäre – wegen der Eliminierbarkeit der Schnittregel – auch selbst eine gültige Sequenz im Kalkül, was per definitionem von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bot} nicht möglich ist. Typisch für diese Widerspruchsfreiheitsbeweise ist, dass in einer Herleitung nur Teilformeln derjenigen Formeln auftreten, die in der hergeleiteten Endsequenz (also unter dem Schlussstrich) vorkommen.

Widerspruchsfreiheitsbeweise der Mathematik werden durchgeführt, indem man, wie Gerhard Gentzen, die transfinite Induktion oder, wie Kurt Schütte und Paul Lorenzen, die sogenannte Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \omega} -Regel in die Beweise des Hauptsatzes einbindet (vollständiger Halbformalismus).

Bedeutung und Anwendungen

Die Entfernung von Schnitten ist nicht nur eine Möglichkeit, die Gültigkeit der Schnittregel 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). Die Ausführung eines Prolog-Programms (d. h. das, was passiert, während das Prolog-Programm ablä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 in der Regel länger als bei Verwendung der Schnittregel. In seinem Artikel "Don't Eliminate Cut!" zeigte der Mathematiker und Logiker George Boolos, dass es eine Formel gibt, die sich unter Zuhilfenahme des Schnitts in etwa einer Seite herleiten lässt, während es länger als die gesamte Lebenszeit des Universums dauern würde, eine Herleitung aufzuschreiben, die ohne Schnitt auskommt.

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 sogenannte verschärfte Hauptsatz ist dem Satz von Herbrand ä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 Kreiser: Logik-Texte, Berlin (Ost) 1986. Teil 1 und Teil 2
• Stephen Cole 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), S. 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 (PDF; 1,3 MB). Nonclassical Logics and Information Processing, S. 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 (PDF; 925 kB)
• Sakharov, Alex. Cut Elimination Theorem. From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.
• Rüdiger Inhetveen: Logik. Eine dialog-orientierte Einführung, Leipzig 2003 ISBN 3-937219-02-1
• William W. Tait, Gödels reformulation of Gentzen's first consistency proof for arithmetic (PDF; 236 kB). Englischer Artikel in: The Bulletin of Symbolic Logic 11(2): S. 225–238, 2005