Gentzenscher Hauptsatz - de.LinkFang.org

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.

Inhaltsverzeichnis

Die Schnittregel


Die Schnittregel ist der modus ponens auf metalogischer Stufe:

Angenommen, die Sequenzen {\displaystyle \Gamma \vdash A} und {\displaystyle A,\Delta \vdash B} sind herleitbar. Die Schnittregel besagt, dass man dann zu der Sequenz \Gamma ,\Delta \vdash B übergehen kann, d. h. die Formel B ist dann auch ohne A herleitbar.

Die griechischen Buchstaben \Gamma und \Delta stehen dabei für Listen von Formeln, die bereits hergeleitet wurden. Für die Herleitbarkeit wird hier das Zeichen \vdash benutzt.

Beweisskizze


Beweise für diesen Hauptsatz liegen inzwischen in einfacher Form vor.[1] 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 A durch (Teilformelinduktion).

Induktionsanfang (n=1): Wenn A nur eine Teilformel besitzt, also nicht zusammengesetzt ist, muss A eine Prim- bzw. Atomformel a sein:

{\frac {\Gamma \vdash a\qquad a,\Delta \vdash \ B}{\Gamma ,\Delta \vdash \ B}} .

Im einfachsten Fall wird a in der Herleitung a,\Delta \vdash B nicht verwendet. Dann ist diese Herleitung auch ohne a gültig, d. h. \Delta \vdash B. Das bedeutet aber, dass B ohne die Schnittregel hergeleitet werden kann.

Wenn hingegen a in der Herleitung a,\Delta \vdash B vorkommt, so kann man darin a durch die Herleitung \Gamma \vdash a ersetzen. Auch in diesem Fall gibt es also eine Möglichkeit, B ohne die Schnittregel herzuleiten.

Induktionsschritt (n zu n+1): Die Induktionsannahme besagt, dass die Schnittregel für die Formeln A gültig ist, die n Teilformeln haben:

{\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[2] benutzen zur technischen Vereinfachung der Beweisführung zusätzlich die aus der Schnittregel beweisbare sogenannte Mischregel (Mix):

{\frac {\Gamma \vdash M\qquad \Delta \vdash \ B}{\Gamma ,(\Delta -M)\vdash B}} .

M heißt Mischformel und \Delta -M bezeichnet die Formelfolge, die entsteht, wenn man in \Delta jedes vorkommende M streicht.

Widerspruchsfreiheit


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

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

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

{\frac {\Gamma \vdash A\qquad \Gamma ,A\vdash \ \bot }{\Gamma \vdash \ \bot }}

so folgt aus der Herleitbarkeit von A und der (gerade erwähnten) von \neg A (beides zusammen ist ein Widerspruch in den Prämissen) die Herleitbarkeit vom unherleitbaren \bot , was nicht sein kann.[3] \Gamma \vdash \ \bot wäre – wegen der Eliminierbarkeit der Schnittregel – auch selbst eine gültige Sequenz im Kalkül, was per definitionem von \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 \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.

Quellen


  1. Inhetveen 2003 (dialogischer Beweis), S. 197; Heindorf 1994, S. 105; Lorenzen 2000 (dialogischer Beweis), S. 81
  2. siehe Gentzen und Heindorf
  3. Dies ist der Grundgedanke bei Paul Lorenzen in der Metamathematik und im Lehrbuch d.k.W. 2000 S. 80ff

Literatur





Kategorien: Mathematische Logik | Satz (Mathematik) | Berechenbarkeitstheorie


Quelle: Wikipedia - https://de.wikipedia.org/wiki/Gentzenscher Hauptsatz (Autoren [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Veränderungen: Alle Bilder und die meisten Designelemente, die mit ihnen in Verbindung stehen, wurden entfernt. Icons wurden teilweise durch FontAwesome-Icons ersetzt. Einige Vorlagen wurden entfernt (wie „Lesenswerter Artikel“, „Exzellenter Artikel“) oder umgeschrieben. CSS-Klassen wurden zum Großteil entfernt oder vereinheitlicht.
Wikipedia spezifische Links, die nicht zu Artikeln oder Kategorien führen (wie „Redlink“, „Bearbeiten-Links“, „Portal-Links“) wurden entfernt. Alle externen Links haben ein zusätzliches FontAwesome Icon erhalten. Neben weiteren kleinen Designanpassungen wurden Media-Container, Karten, Navigationsboxen, gesprochene Versionen & Geo-Mikroformate entfernt.


Stand der Informationen: 23.10.2019 09:46:04 CEST - Wichtiger Hinweis Da die gegebenen Inhalte zum angegebenen Zeitpunkt maschinell von Wikipedia übernommen wurden, war und ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.org nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein oder Fehler in der Darstellung vorliegen, bitten wir Sie darum uns per zu kontaktieren: E-Mail.
Beachten Sie auch : Impressum & Datenschutzerklärung.