www.wikidata.de-de.nina.az

Gentzenscher Hauptsatz Der Gentzensche Hauptsatz oder Schnittsatz englisch cut elimination theorem ist ein Satz der math

Gentzenscher Hauptsatz

Der Gentzensche Hauptsatz oder Schnittsatz (englisch cut-elimination theorem) ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in jeder Herleitung eines Gentzentypkalküls eliminierbar und damit zulässig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies.

Der Hauptsatz Bearbeiten

Gerhard Gentzen stellte in den 1930er Jahren die Sequenzenkalküle LJ und LK und die Systeme des natürlichen Schließens NJ und NK (J ist jeweils der intuitionistische und K der klassische Kalkül) auf. Eine Herleitungsregel in diesen Kalkülen ist die Schnittregel oder kurz der Schnitt. Das ist der modus ponens auf metalogischer Stufe. Gentzen entdeckte, dass man bei jeder Herleitung in diesen Kalkülen auf den Schnitt verzichten kann:

Sind die Sequenzen und herleitbar, so besagt die Schnittregel, dass man dann zu der Sequenz übergehen kann. Die Formel A wird also weggeschnitten.

Der Gentzensche Hauptsatz besagt nun, dass man diese Schnittregel, überall wo sie in Herleitungen benutzt wird, durch andere Regeln des Kalküls ersetzen kann.

Beweisskizze Bearbeiten

Die Grundidee des Beweises 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 durch (Teilformelinduktion).

Induktionsanfang (): Wenn nur aus einer Teilformel besteht:

kann die Herleitung von aus einfach übernommen werden.

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

Nun wird eine Fallunterscheidung in Bezug auf das in:

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 (nicht-dialogischen) Beweise benutzen zur technischen Vereinfachung der Beweisführung zusätzlich die aus der Schnittregel beweisbare sogenannte Mischregel (Mix):

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

Widerspruchsfreiheit Bearbeiten

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

Ein Gedankengang für den Beweis der Widerspruchsfreiheit ist folgender: Sei (lies: falsch oder falsum) per definitionem nicht herleitbar. Dann ist nichts anderes als die Herleitbarkeit von Die Negation ist dieser Spezialfall der Subjunktion.

Setzt man nun für in die Schnittregel ein:

so folgt aus der Herleitbarkeit von und der (gerade erwähnten) von (beides zusammen ist ein Widerspruch in den Prämissen) die Herleitbarkeit vom unherleitbaren , was nicht sein kann. wäre – wegen der Eliminierbarkeit der Schnittregel – auch selbst eine gültige Sequenz im Kalkül, was per definitionem von 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 ω-Regel in die Beweise des Hauptsatzes einbindet (vollständiger Halbformalismus).

Bedeutung und Anwendungen Bearbeiten

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 Bearbeiten

  1. Gentzen: Untersuchung über das logische Schließen. In: Mathematische Zeitschrift 39, 1934, 176–210.
  2. Die griechischen Buchstaben und stehen dabei für Listen von Formeln, die bereits hergeleitet wurden. Für die Herleitbarkeit wird hier das Zeichen benutzt.
  3. Dies ist der Grundgedanke bei Paul Lorenzen in der Metamathematik und im Lehrbuch d.k.W. 2000 S. 80ff

Literatur Bearbeiten

  • 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, auch: Untersuchung über das logische Schließen.
  • Christian Thiel: Gentzenscher Hauptsatz. In: Jürgen Mittelstraß (Hrsg.): Enzyklopädie Philosophie und Wissenschaftstheorie. Zweite Auflage. Band 3, Metzler 2008, S. 84f.
  • Paul Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Zürich 1987, reprint Stuttgart 2000, ISBN 3-476-01784-2
  • Kurt Schütte: Beweistheorie, Berlin Göttingen Heidelberg 1960
  • 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 (Hrsg.): 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.
  • Sakharov, Alex. Cut Elimination Theorem. From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein.
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Der Gentzensche Hauptsatz oder Schnittsatz englisch cut elimination theorem ist ein Satz der mathematischen Logik der besagt dass die Schnittregel in jeder Herleitung eines Gentzentypkalkuls eliminierbar und damit zulassig ist Er ist nach Gerhard Gentzen benannt der ihn 1934 aufstellte und bewies 1 Inhaltsverzeichnis 1 Der Hauptsatz 2 Beweisskizze 3 Widerspruchsfreiheit 4 Bedeutung und Anwendungen 5 Quellen 6 LiteraturDer Hauptsatz BearbeitenGerhard Gentzen stellte in den 1930er Jahren die Sequenzenkalkule LJ und LK und die Systeme des naturlichen Schliessens NJ und NK J ist jeweils der intuitionistische und K der klassische Kalkul auf Eine Herleitungsregel in diesen Kalkulen ist die Schnittregel oder kurz der Schnitt Das ist der modus ponens auf metalogischer Stufe Gentzen entdeckte dass man bei jeder Herleitung in diesen Kalkulen auf den Schnitt verzichten kann Sind die Sequenzen G A displaystyle Gamma vdash A nbsp und A D B displaystyle A Delta vdash B nbsp herleitbar so besagt die Schnittregel dass man dann zu der Sequenz G D B displaystyle Gamma Delta vdash B nbsp ubergehen kann Die Formel A wird also weggeschnitten 2 Der Gentzensche Hauptsatz besagt nun dass man diese Schnittregel uberall wo sie in Herleitungen benutzt wird durch andere Regeln des Kalkuls ersetzen kann Beweisskizze BearbeitenDie Grundidee des Beweises ist Herleitungen in denen die Schnittregel verwendet wird so aufzulosen englisch cut elimination dass sie nicht mehr verwendet wird Dazu fuhrt man eine vollstandige Induktion uber die Anzahl der Teilformeln in der Schnittformel A displaystyle A nbsp durch Teilformelinduktion Induktionsanfang n 1 displaystyle n 1 nbsp Wenn A displaystyle A nbsp nur aus einer Teilformel a displaystyle a nbsp besteht G a a D B G D B displaystyle frac Gamma vdash a qquad a Delta vdash B Gamma Delta vdash B nbsp kann die Herleitung von a displaystyle a nbsp aus G displaystyle Gamma nbsp einfach ubernommen werden Induktionsschritt n displaystyle n nbsp zu n 1 displaystyle n 1 nbsp Die Induktionsannahme besagt dass die Schnittregel fur die Formeln A displaystyle A nbsp gultig ist die n Teilformeln haben G A n A n D B G D B displaystyle frac Gamma vdash A n qquad A n Delta vdash B Gamma Delta vdash B nbsp Nun wird eine Fallunterscheidung in Bezug auf das in G A n 1 A n 1 D B G D B displaystyle frac Gamma vdash A n 1 qquad A n 1 Delta vdash B Gamma Delta vdash B nbsp neu hinzukommende Logikzeichen durchgefuhrt die Schnittregel wird also jeweils durch die Kalkulregeln fur dieses Zeichen ersetzt Bei den Junktoren ist dieser Beweisteil trotz der vielen Fallunterscheidungen relativ einfach Bei den Quantoren wird im dialogischen Beweis uber die Anzahl der Entwicklungsschritte induziert Die nicht dialogischen Beweise benutzen zur technischen Vereinfachung der Beweisfuhrung zusatzlich die aus der Schnittregel beweisbare sogenannte Mischregel Mix G M D B G D M B displaystyle frac Gamma vdash M qquad Delta vdash B Gamma Delta M vdash B nbsp M displaystyle M nbsp heisst Mischformel und D M displaystyle Delta M nbsp bezeichnet die Formelfolge die entsteht wenn man in D displaystyle Delta nbsp jedes vorkommende M displaystyle M nbsp streicht Widerspruchsfreiheit BearbeitenDie Kalkule fur die der Hauptsatz gilt sind widerspruchsfrei Ein Gedankengang fur den Beweis der Widerspruchsfreiheit ist folgender Sei displaystyle bot nbsp lies falsch oder falsum per definitionem nicht herleitbar Dann ist A displaystyle A vdash bot nbsp nichts anderes als die Herleitbarkeit von A displaystyle neg A nbsp Die Negation ist dieser Spezialfall der Subjunktion Setzt man nun fur B displaystyle B nbsp in die Schnittregel displaystyle bot nbsp ein G A G A G displaystyle frac Gamma vdash A qquad Gamma A vdash bot Gamma vdash bot nbsp so folgt aus der Herleitbarkeit von A displaystyle A nbsp und der gerade erwahnten von displaystyle neg nbsp A displaystyle A nbsp beides zusammen ist ein Widerspruch in den Pramissen die Herleitbarkeit vom unherleitbaren displaystyle bot nbsp was nicht sein kann 3 G displaystyle Gamma vdash bot nbsp ware wegen der Eliminierbarkeit der Schnittregel auch selbst eine gultige Sequenz im Kalkul was per definitionem von displaystyle bot nbsp nicht moglich ist Typisch fur 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 durchgefuhrt indem man wie Gerhard Gentzen die transfinite Induktion oder wie Kurt Schutte und Paul Lorenzen die w Regel in die Beweise des Hauptsatzes einbindet vollstandiger Halbformalismus Bedeutung und Anwendungen BearbeitenDie Entfernung von Schnitten ist nicht nur eine Moglichkeit die Gultigkeit der Schnittregel zu beweisen sondern umgedreht ein sehr nutzliches mathematisch logisches Werkzeug beispielsweise beim Beweis des Interpolation Theorems von Craig und Schutte Die Moglichkeit Beweise durchzufuhren die auf Resolution beruhen ist sehr machtig Maschinengestutztes Beweisen Die Ausfuhrung eines Prolog Programms d h das was passiert wahrend das Prolog Programm ablauft lasst sich als schnittfreie Kalkul Herleitung interpretieren Fuhrt man allerdings in Gentzentypkalkulen Beweise durch die den Schnitt vermeiden analytic proofs so sind diese in der Regel langer 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 lasst wahrend es langer als die gesamte Lebenszeit des Universums dauern wurde 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 verscharfte Hauptsatz ist dem Satz von Herbrand ahnlich Dabei geht es um die Rolle der Quantoren in einem Beweis Quellen Bearbeiten Gentzen Untersuchung uber das logische Schliessen In Mathematische Zeitschrift 39 1934 176 210 Die griechischen Buchstaben G displaystyle Gamma nbsp und D displaystyle Delta nbsp stehen dabei fur Listen von Formeln die bereits hergeleitet wurden Fur die Herleitbarkeit wird hier das Zeichen displaystyle vdash nbsp benutzt Dies ist der Grundgedanke bei Paul Lorenzen in der Metamathematik und im Lehrbuch d k W 2000 S 80ffLiteratur BearbeitenGerhard Gentzen Untersuchungen uber das logische Schliessen Mathematische Zeitschrift 39 1934 Nachdruck in Karel Berka Lothar Kreiser Logik Texte Berlin Ost 1986 Teil 1 und Teil 2 auch Untersuchung uber das logische Schliessen Christian Thiel Gentzenscher Hauptsatz In Jurgen Mittelstrass Hrsg Enzyklopadie Philosophie und Wissenschaftstheorie Zweite Auflage Band 3 Metzler 2008 S 84f Paul Lorenzen Lehrbuch der konstruktiven Wissenschaftstheorie Zurich 1987 reprint Stuttgart 2000 ISBN 3 476 01784 2 Kurt Schutte Beweistheorie Berlin Gottingen Heidelberg 1960 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 Hrsg 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 Sakharov Alex Cut Elimination Theorem From MathWorld A Wolfram Web Resource created by Eric W Weisstein Abgerufen von https de wikipedia org w index php title Gentzenscher Hauptsatz amp oldid 231064648