www.wikidata.de-de.nina.az

Sequenzenkalkül In der Beweistheorie und der mathematischen Logik bezeichnet man mit formale Systeme oder Kalküle die ei

Sequenzenkalkül

In der Beweistheorie und der mathematischen Logik bezeichnet man mit Sequenzenkalkül formale Systeme (oder Kalküle), die einen bestimmten Stil der Ableitung und gewisse Eigenschaften teilen. Die ersten Sequenzenkalküle, LK für die klassische und LJ für die intuitionistische Logik, sind von Gerhard Gentzen im Jahre 1934 als formaler Rahmen für die Untersuchung von Systemen des natürlichen Schließens in der Prädikatenlogik 1. Ordnung eingeführt worden.

Der Gentzensche Hauptsatz über LK und LJ besagt, dass die Schnittregel in diesen Systemen gilt, ein Satz mit weitreichenden Konsequenzen in der Metalogik. Die Flexibilität des Sequenzenkalküls zeigte sich später, im Jahr 1936, als Gentzen die Technik der Schnitt-Elimination verwendete, um die Widerspruchsfreiheit der Peano-Arithmetik zu beweisen.

Die auf Gentzen zurückgehenden Sequenzenkalküle und die allgemeinen Konzepte, die dahinterstehen, werden in weiten Bereichen der Beweistheorie, mathematischen Logik und des maschinengestützten Beweisens standardmäßig verwendet.

Notationen und Konventionen Bearbeiten

In diesem Artikel werden folgende Zeichen verwendet:

  • , …: Formelmengen
  • , , …: Formeln der Prädikatenlogik
  •  : Zeichen für Herleitungsbeziehung
  • ,  : Zeichen für die Beziehung der logischen Wahrheit/Folge
  •  : Negationszeichen
  •  : Adjunktionszeichen
  •  : Existenzquantor
  • ,  : Klammern als Hilfszeichen für mehr Übersichtlichkeit
  •  : Kennzeichnung für die Erweiterung einer Formelmenge
  •  : Zeichen für Modell
  •  : (Zeichen für Variablenbelegungsfunktion)

Es werden folgende Konventionen eingeführt:

  • Mittels diverser Regeln lassen sich die übrigen Junktoren in Formeln umformen, die dann nur noch und enthalten. Die Umformungregeln folgen:
  • Mittels einer Umformungsregel lässt sich der Quantor (Allquantor) wie folgt darstellen:

Von diesen Umformungen wird in den Beispielen Gebrauch gemacht.

Einleitung Bearbeiten

Der Sequenzenkalkül dient dazu, das Vorgehen beim mathematischen Beweisen von Theoremen möglichst genau abzubilden. Ein Bestandteil dieser Beweismethode ist, dass an jeder Stelle des Beweises Zusatzvoraussetzungen eingebracht werden können, die dann entweder bis zum Schluss stehen bleiben oder aber wieder eliminiert werden können.

Die Grundeinheit des Sequenzenkalküls ist eine Zeichenfolge (eine Sequenz) aus Variablen , die jeweils für Ausdrücke des jeweils betrachteten logischen Systems stehen; z. B. für Ausdrücke einer Sprache erster Stufe. Eine solche Sequenz bezeichnen wir mit

oder kürzer mit

wobei für die Folge der Ausdrücke steht. Die Idee dabei ist, dass in die Voraussetzungen stehen und das letzte Glied die Folgerung aus diesen Voraussetzungen bezeichnet. Die Voraussetzungen werden auch als Antezedens bezeichnet und die Folgerung als Sukzedens. Während in der hier dargestellten Variante des Kalküls das Sukzedens aus nur einer Formel besteht, lassen andere Varianten, darunter Gentzens LK, beliebig viele Formeln im Sukzedens zu.

Der Sequenzenkalkül beschäftigt sich mit der Ableitung von Sequenzen. Gibt es im Kalkül eine Ableitung der Sequenz , dann schreibt man auch

Definition: Der Ausdruck heißt aus ableitbar (kurz: ), wenn es aus gibt mit .

Die Sequenzenregeln: Allgemeine Gestalt Bearbeiten

Im Folgenden werden die Regeln für den Sequenzenkalkül der klassischen Prädikatenlogik erster Stufe aufgeführt. Sequenzenregeln haben dabei die allgemeine Gestalt

Oberhalb des Striches stehen bereits abgeleitete Sequenzen, und unterhalb die daraus ableitbare Sequenz.

Andere Schreibweise Bearbeiten

Sequenzenregeln findet man in der Literatur auch in der Form

oder auch als

notiert.

Regeln des Sequenzenkalküls der Prädikatenlogik erster Stufe mit Identität Bearbeiten

Die Regeln des Sequenzenkalküls der Prädikatenlogik erster Stufe mit Identität werden in folgende Gruppen eingeteilt:

Grundregeln, Junktorenregeln, Quantorenregeln und Identitätsregeln.

Grundregeln Bearbeiten

Zu den Grundregeln gehören die Antezedensregel und die Annahmeregel.

Antezedensregel Bearbeiten

wobei gilt:

In Worten: Man kann problemlos Annahmen hinzufügen.

Annahmeregel Bearbeiten

In Worten: Man kann Annahmen aus denselben schließen.

Junktorenregeln Bearbeiten

Zu den Junktorenregeln gehören die Fallunterscheidung, die Kontradiktion, die Adjunktionseinführung im Antezedens und die Adjunktionseinführung im Konsequens.

Fallunterscheidung Bearbeiten

In Worten: Wenn man einerseits unter der Annahme von und andererseits unter der Annahme von herleiten kann, darf man, ohne irgendeine Annahme über oder machen zu müssen, auf schließen.

Kontradiktion Bearbeiten

In Worten: Wenn zu einem Widerspruch führt, dann darf auf geschlossen werden.

Adjunktionseinführung im Antezedens Bearbeiten

In Worten: Disjunktionen der Form im Antezedens können auf zwei Weisen verwendet werden – einerseits im Fall und andererseits im Fall .

Adjunktionseinführung im Konsequens Bearbeiten

In Worten: Man darf immer das Konsequens durch eine Adjunktionseinführung abschwächen.

Quantorenregeln Bearbeiten

Zu den Quantorenregeln gehören die Existenzeinführung im Konsequens und die Existenzeinführung im Antezedens.

Existenzeinführung im Konsequens Bearbeiten

In Worten: Wenn man aus herleiten kann, dass eine durch ausgedrückte Eigenschaft hat, dann darf man auch darauf schließen, dass etwas existiert, welches eine Eigenschaft hat, die durch ausgedrückt wird.

Existenzeinführung im Antezedens Bearbeiten

Identitätsregeln Bearbeiten

Zu den Identitätsregeln gehören die Reflexivität und die Substitutionsregel.

Reflexivität Bearbeiten

In Worten: Die Äquivalenzrelation auf dem Gegenstandsbereich ist reflexiv.

Substitutionsregel Bearbeiten

In Worten: Einsetzung von Identischem in Identisches.

Nützliche Herleitungen Bearbeiten

Mit den oben aufgestellten Regeln des Sequenzenkalküls werden nun in endlich vielen Schritten einige weitere nützliche Regeln hergeleitet. Zur Unterscheidung von den obigen Grundregeln heißen sie auch abgeleitete Regeln. (Zur Erinnerung: Herleitung ist gleichzusetzen mit Sequenzenmanipulation durch Anwendung der Regeln.) Diese einmal abgeleiteten Regeln können dann problemlos verwendet werden, das heißt, es reicht, deren Herleitung hier einmal zu zeigen. Hier werden folgende Regeln bewiesen: der Satz vom ausgeschlossenen Dritten, die Trivialität, der Kettenschluss, die Kontraposition und der disjunktive Syllogismus. Zur Notation: Jede Herleitung ist in drei Spalten aufgeteilt. In der linken Spalte befindet sich die Nummerierung der einzelnen Modifikationen. Sie sind für eine unmissverständliche Bezugnahme durch andere Modifikationen nützlich. Die mittlere Spalte enthält die neue Modifikation, mit einer Abfolge von Sequenzen als Ergebnis. Die rechte Spalte enthält die Information, wie die Sequenz in der mittleren Spalte erreicht wurde. Dabei ist die Regel in Klammern geschrieben, und eventuell, durch ein Doppelpunkt eingeleitet (zu lesen als „angewendet auf“), sind die für das Ergebnis relevanten Zeilennummern notiert. Bsp.: „(Ant):1.,2.“ wird gelesen als „Antezedensregel, angewendet auf Zeile eins und zwei“.

Satz vom ausgeschlossenen Dritten Bearbeiten

Herleitung:

Trivialität Bearbeiten

Herleitung:

Kettenschluss Bearbeiten

Herleitung:

Anmerkung: Bei dieser Herleitung wurde die Regel (Triv) verwendet. An diesem Beispiel sieht man, dass eine Regel bloß einmal fehlerfrei hergeleitet zu werden braucht; in der Folge kann sie als Abkürzung verwendet werden. Durch die Verwendung der Regel (Triv) wurden fünf Herleitungsschritte ausgespart (nämlich genau die fünf Schritte, die man benötigt, um (Triv) herzuleiten).

Kontraposition Bearbeiten

Herleitung von (KP1):

Die Aussagen (KP2) bis (KP4) lassen sich analog beweisen.

Disjunktiver Syllogismus Bearbeiten

Herleitung:

Eigenschaften des Sequenzenkalküls Bearbeiten

Korrektheit Bearbeiten

Der Korrektheitssatz lautet wie folgt:

Für alle Formelmengen und alle Formeln gilt: Wenn , dann .

Die Korrektheit des Sequenzenkalküls wird dadurch gezeigt, dass für jede einzelne Regel des Sequenzenkalküls gezeigt wird, dass sie korrekt ist, das heißt, dass jedes Modell und jede Variablenbelegung s, die die Prämissen der Regel wahr machen, auch deren Konsequenz wahr machen. Alle Korrektheitsbeweise zusammengenommen ergeben dann den Beweis des Korrektheitssatzes.

Definitionen Bearbeiten

Um den Korrektheitssatz zeigen zu können, müssen zuvor noch „Modell“, „Variablenbelegung“ und „wahr machen“ (logische Wahrheit) definiert werden.

Modell Bearbeiten

Ein Modell ist ein geordnetes Paar , sodass gilt:

  1. ist eine nicht-leere Menge (der Träger oder der Gegenstandsbereich, englisch domain, über den die Quantoren laufen)
  2. ist die Interpretationsfunktion für Prädikate, Funktionen und Konstanten (in der Folge nicht relevant)
Variablenbelegung Bearbeiten

Eine Variablenbelegung s über einem Modell ist eine Funktion .

Logische Wahrheit/Folge Bearbeiten

Für alle Formeln und alle Formelmengen gilt: folgt logisch aus (kurz: ) gdw für alle Modelle und alle Variablenbelegungen s über gilt: Wenn , dann . (M.a.W.: Jedes , das wahr macht, macht auch wahr.)

Korrektheit der Regeln des Sequenzenkalküls Bearbeiten

Die Korrektheit der Regeln des Sequenzenkalküls zeigt man, indem man die logische Wahrheit der Regeln zeigt. Dabei stützt man sich auf die Definition der logischen Wahrheit/Folge. Nun wird gezeigt, dass jede einzelne Regel des Sequenzenkalküls logisch wahr ist. (Es werden nicht alle Beweise gezeigt. Es reicht, lediglich einige wenige zu skizzieren. Die restlichen Beweise sind von der Struktur her ähnlich.)

Korrektheit von (Ant) Bearbeiten

Angenommen, ist korrekt, d. h. . Sei eine Formelmenge, sodass gilt: . Seien beliebig gewählt, sodass gilt: . Dann gilt auch und laut Voraussetzung auch . Daraus folgt . Also ist korrekt.

Korrektheit von (Ann) Bearbeiten

Wenn , dann gilt . Somit ist korrekt.

Korrektheit von (FU) Bearbeiten

Angenommen und sind korrekt, d. h. und . Seien beliebig gewählt, sodass gilt: .

Fall 1: . Dann und somit nach Voraussetzung .

Fall 2: . Dann . Dann und somit nach Voraussetzung .

In beiden Fällen gilt . Somit ist korrekt.

Korrektheit von (KD) Bearbeiten

Angenommen und . Dann gilt für alle mit :

und . Dann gibt es kein , sodass gilt: . Dann gilt für alle mit : . Somit gilt und somit ist korrekt.

Hat man noch zusätzlich die restlichen Regeln bewiesen, also deren Korrektheit gezeigt, so ist der Korrektheitssatz bewiesen und es kann gesagt werden: Ist eine Formel im Sequenzenkalkül herleitbar, so ist diese Formel auch logisch wahr.

Vollständigkeit Bearbeiten

Der Kalkül ist außerdem auch noch vollständig. Das heißt, es gilt:

Für alle Formelmengen und alle Formeln gilt: Wenn , dann .

Intuitiv bedeutet dies, dass alle wahren Sequenzen mit Hilfe der oben angegebenen Regeln hergeleitet werden können.

Beispiele Bearbeiten

Zum Schluss sollen noch zwei Beispiele mit dem Sequenzenkalkül vorgeführt werden.

Beispiel 1 Bearbeiten

Herleitung:

Beispiel 2 Bearbeiten

Herleitung:

Literatur Bearbeiten

  • Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik. Berlin: Springer-Verlag, 2007.
  • Gerhard Gentzen (hrsg. M. E. Szabo): The Collected Papers of Gerhard Gentzen, Amsterdam 1969.
  • Wolfgang Rautenberg: Einführung in die Mathematische Logik. Ein Lehrbuch. 3., überarbeitete Auflage. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2.
  • Gaisi Takeuti: Proof theory (= Studies in logic and the foundations of mathematics. Band 81). 2. Auflage. North-Holland, Amsterdam 1987, ISBN 0-444-87943-9.
  • Richter, M. M.: Logikkalküle. Stuttgart: Teubner Verlag, 1978.
  • A. S. Troelstra, H. Schwichtenberg. Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, ISBN 0-521-77911-1.

Weblinks Bearbeiten

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:
In der Beweistheorie und der mathematischen Logik bezeichnet man mit Sequenzenkalkul formale Systeme oder Kalkule die einen bestimmten Stil der Ableitung und gewisse Eigenschaften teilen Die ersten Sequenzenkalkule LK fur die klassische und LJ fur die intuitionistische Logik sind von Gerhard Gentzen im Jahre 1934 als formaler Rahmen fur die Untersuchung von Systemen des naturlichen Schliessens in der Pradikatenlogik 1 Ordnung eingefuhrt worden Der Gentzensche Hauptsatz uber LK und LJ besagt dass die Schnittregel in diesen Systemen gilt ein Satz mit weitreichenden Konsequenzen in der Metalogik Die Flexibilitat des Sequenzenkalkuls zeigte sich spater im Jahr 1936 als Gentzen die Technik der Schnitt Elimination verwendete um die Widerspruchsfreiheit der Peano Arithmetik zu beweisen Die auf Gentzen zuruckgehenden Sequenzenkalkule und die allgemeinen Konzepte die dahinterstehen werden in weiten Bereichen der Beweistheorie mathematischen Logik und des maschinengestutzten Beweisens standardmassig verwendet Inhaltsverzeichnis 1 Notationen und Konventionen 2 Einleitung 3 Die Sequenzenregeln Allgemeine Gestalt 3 1 Andere Schreibweise 4 Regeln des Sequenzenkalkuls der Pradikatenlogik erster Stufe mit Identitat 4 1 Grundregeln 4 1 1 Antezedensregel 4 1 2 Annahmeregel 4 2 Junktorenregeln 4 2 1 Fallunterscheidung 4 2 2 Kontradiktion 4 2 3 Adjunktionseinfuhrung im Antezedens 4 2 4 Adjunktionseinfuhrung im Konsequens 4 3 Quantorenregeln 4 3 1 Existenzeinfuhrung im Konsequens 4 3 2 Existenzeinfuhrung im Antezedens 4 4 Identitatsregeln 4 4 1 Reflexivitat 4 4 2 Substitutionsregel 5 Nutzliche Herleitungen 5 1 Satz vom ausgeschlossenen Dritten 5 2 Trivialitat 5 3 Kettenschluss 5 4 Kontraposition 5 5 Disjunktiver Syllogismus 6 Eigenschaften des Sequenzenkalkuls 6 1 Korrektheit 6 1 1 Definitionen 6 1 1 1 Modell 6 1 1 2 Variablenbelegung 6 1 1 3 Logische Wahrheit Folge 6 1 2 Korrektheit der Regeln des Sequenzenkalkuls 6 1 2 1 Korrektheit von Ant 6 1 2 2 Korrektheit von Ann 6 1 2 3 Korrektheit von FU 6 1 2 4 Korrektheit von KD 6 2 Vollstandigkeit 7 Beispiele 7 1 Beispiel 1 7 2 Beispiel 2 8 Literatur 9 WeblinksNotationen und Konventionen BearbeitenIn diesem Artikel werden folgende Zeichen verwendet G displaystyle Gamma nbsp F displaystyle Phi nbsp Formelmengen f displaystyle varphi nbsp ps displaystyle psi nbsp r displaystyle rho nbsp Formeln der Pradikatenlogik displaystyle vdash nbsp Zeichen fur Herleitungsbeziehung displaystyle vDash nbsp displaystyle nvDash nbsp Zeichen fur die Beziehung der logischen Wahrheit Folge displaystyle neg nbsp Negationszeichen displaystyle vee nbsp Adjunktionszeichen displaystyle exists nbsp Existenzquantor displaystyle nbsp displaystyle nbsp Klammern als Hilfszeichen fur mehr Ubersichtlichkeit displaystyle nbsp Kennzeichnung fur die Erweiterung einer Formelmenge M displaystyle mathfrak M nbsp Zeichen fur Modell s displaystyle s nbsp Zeichen fur Variablenbelegungsfunktion Es werden folgende Konventionen eingefuhrt Mittels diverser Regeln lassen sich die ubrigen Junktoren displaystyle wedge rightarrow leftrightarrow nbsp in Formeln umformen die dann nur noch displaystyle neg nbsp und displaystyle vee nbsp enthalten Die Umformungregeln folgen f ps f ps displaystyle varphi wedge psi Leftrightarrow neg neg varphi vee neg psi nbsp f ps f ps displaystyle varphi rightarrow psi Leftrightarrow neg varphi vee psi nbsp f ps f ps ps f displaystyle varphi leftrightarrow psi Leftrightarrow neg neg neg varphi vee psi vee neg neg psi vee varphi nbsp Mittels einer Umformungsregel lasst sich der Quantor displaystyle forall nbsp Allquantor wie folgt darstellen x f x f displaystyle forall x varphi Leftrightarrow neg exists x neg varphi nbsp Von diesen Umformungen wird in den Beispielen Gebrauch gemacht Einleitung BearbeitenDer Sequenzenkalkul dient dazu das Vorgehen beim mathematischen Beweisen von Theoremen moglichst genau abzubilden Ein Bestandteil dieser Beweismethode ist dass an jeder Stelle des Beweises Zusatzvoraussetzungen eingebracht werden konnen die dann entweder bis zum Schluss stehen bleiben oder aber wieder eliminiert werden konnen Die Grundeinheit des Sequenzenkalkuls ist eine Zeichenfolge eine Sequenz aus Variablen ϕ i ϕ displaystyle phi i phi nbsp die jeweils fur Ausdrucke des jeweils betrachteten logischen Systems stehen z B fur Ausdrucke einer Sprache erster Stufe Eine solche Sequenz bezeichnen wir mit ϕ 1 ϕ 2 ϕ n ϕ displaystyle phi 1 phi 2 dots phi n phi nbsp oder kurzer mit G ϕ displaystyle Gamma phi nbsp wobei G displaystyle Gamma nbsp fur die Folge der Ausdrucke ϕ 1 ϕ n displaystyle phi 1 dots phi n nbsp steht Die Idee dabei ist dass in G displaystyle Gamma nbsp die Voraussetzungen stehen und das letzte Glied ϕ displaystyle phi nbsp die Folgerung aus diesen Voraussetzungen bezeichnet Die Voraussetzungen werden auch als Antezedens bezeichnet und die Folgerung als Sukzedens Wahrend in der hier dargestellten Variante des Kalkuls das Sukzedens aus nur einer Formel besteht lassen andere Varianten darunter Gentzens LK beliebig viele Formeln im Sukzedens zu Der Sequenzenkalkul beschaftigt sich mit der Ableitung von Sequenzen Gibt es im Kalkul eine Ableitung der Sequenz G ϕ displaystyle Gamma phi nbsp dann schreibt man auch G ϕ displaystyle vdash Gamma phi nbsp Definition Der Ausdruck ϕ displaystyle phi nbsp heisst aus F displaystyle Phi nbsp ableitbar kurz F ϕ displaystyle Phi vdash phi nbsp wenn es ϕ 1 ϕ n displaystyle phi 1 dots phi n nbsp aus F displaystyle Phi nbsp gibt mit ϕ 1 ϕ n ϕ displaystyle vdash phi 1 dots phi n phi nbsp Die Sequenzenregeln Allgemeine Gestalt BearbeitenIm Folgenden werden die Regeln fur den Sequenzenkalkul der klassischen Pradikatenlogik erster Stufe aufgefuhrt Sequenzenregeln haben dabei die allgemeine Gestalt G 1 ϕ 1 G 2 ϕ 2 G n ϕ n G ϕ displaystyle frac Gamma 1 phi 1 Gamma 2 phi 2 dots Gamma n phi n Gamma phi nbsp Oberhalb des Striches stehen bereits abgeleitete Sequenzen und unterhalb die daraus ableitbare Sequenz Andere Schreibweise Bearbeiten Sequenzenregeln findet man in der Literatur auch in der Form G 1 ϕ 1 G 2 ϕ 2 G n ϕ n G ϕ displaystyle frac Gamma 1 vdash phi 1 Gamma 2 vdash phi 2 dots Gamma n vdash phi n Gamma vdash phi nbsp oder auch als G 1 ϕ 1 G 2 ϕ 2 G n ϕ n G ϕ displaystyle frac Gamma 1 Rightarrow phi 1 Gamma 2 Rightarrow phi 2 dots Gamma n Rightarrow phi n Gamma Rightarrow phi nbsp notiert Regeln des Sequenzenkalkuls der Pradikatenlogik erster Stufe mit Identitat BearbeitenDie Regeln des Sequenzenkalkuls der Pradikatenlogik erster Stufe mit Identitat werden in folgende Gruppen eingeteilt Grundregeln Junktorenregeln Quantorenregeln und Identitatsregeln Grundregeln Bearbeiten Zu den Grundregeln gehoren die Antezedensregel und die Annahmeregel Antezedensregel Bearbeiten Ant G f G f displaystyle left text Ant right qquad frac Gamma varphi Gamma varphi nbsp wobei gilt G G displaystyle Gamma subseteq Gamma nbsp In Worten Man kann problemlos Annahmen hinzufugen Annahmeregel Bearbeiten Ann G f displaystyle left text Ann right qquad frac Gamma varphi nbsp wobei gilt f G displaystyle varphi in Gamma nbsp In Worten Man kann Annahmen aus denselben schliessen Junktorenregeln Bearbeiten Zu den Junktorenregeln gehoren die Fallunterscheidung die Kontradiktion die Adjunktionseinfuhrung im Antezedens und die Adjunktionseinfuhrung im Konsequens Fallunterscheidung Bearbeiten FU G ps f G ps f G f displaystyle left text FU right qquad frac begin aligned Gamma psi varphi Gamma neg psi varphi end aligned Gamma varphi nbsp In Worten Wenn man f displaystyle varphi nbsp einerseits unter der Annahme von ps displaystyle psi nbsp und andererseits unter der Annahme von ps displaystyle neg psi nbsp herleiten kann darf man ohne irgendeine Annahme uber ps displaystyle psi nbsp oder ps displaystyle neg psi nbsp machen zu mussen auf f displaystyle varphi nbsp schliessen Kontradiktion Bearbeiten KD G ps r G ps r G ps displaystyle left text KD right qquad frac begin aligned Gamma neg psi rho Gamma neg psi neg rho end aligned Gamma psi nbsp In Worten Wenn ps displaystyle neg psi nbsp zu einem Widerspruch fuhrt dann darf auf ps displaystyle psi nbsp geschlossen werden Adjunktionseinfuhrung im Antezedens Bearbeiten Ant G f r G ps r G f ps r displaystyle left vee text Ant right qquad frac begin aligned Gamma varphi rho Gamma psi rho end aligned Gamma varphi vee psi rho nbsp In Worten Disjunktionen der Form f ps displaystyle varphi vee psi nbsp im Antezedens konnen auf zwei Weisen verwendet werden einerseits im Fall f displaystyle varphi nbsp und andererseits im Fall ps displaystyle psi nbsp Adjunktionseinfuhrung im Konsequens Bearbeiten Kon1 G f G f ps displaystyle left vee text Kon1 right qquad frac begin aligned Gamma varphi end aligned Gamma varphi vee psi nbsp Kon2 G ps G f ps displaystyle left vee text Kon2 right qquad frac begin aligned Gamma psi end aligned Gamma varphi vee psi nbsp In Worten Man darf immer das Konsequens durch eine Adjunktionseinfuhrung abschwachen Quantorenregeln Bearbeiten Zu den Quantorenregeln gehoren die Existenzeinfuhrung im Konsequens und die Existenzeinfuhrung im Antezedens Existenzeinfuhrung im Konsequens Bearbeiten Kon G f t x G x f displaystyle left exists text Kon right qquad frac Gamma varphi frac t x Gamma exists x varphi nbsp In Worten Wenn man aus G displaystyle Gamma nbsp herleiten kann dass t displaystyle t nbsp eine durch f displaystyle varphi nbsp ausgedruckte Eigenschaft hat dann darf man auch darauf schliessen dass etwas existiert welches eine Eigenschaft hat die durch f displaystyle varphi nbsp ausgedruckt wird Existenzeinfuhrung im Antezedens Bearbeiten Ant G f y x ps G x f ps displaystyle left exists text Ant right qquad frac Gamma varphi frac y x psi Gamma exists x varphi psi nbsp wenn y displaystyle y nbsp in der Sequenz x f ps displaystyle exists x varphi psi nbsp nicht frei vorkommt Identitatsregeln Bearbeiten Zu den Identitatsregeln gehoren die Reflexivitat und die Substitutionsregel Reflexivitat Bearbeiten Ref t t displaystyle left text Ref right qquad frac t equiv t nbsp In Worten Die Aquivalenzrelation auf dem Gegenstandsbereich D displaystyle D nbsp ist reflexiv Substitutionsregel Bearbeiten Sub G f t x ps G t t f t x ps displaystyle left exists text Sub right qquad frac Gamma varphi frac t x psi Gamma t equiv t varphi frac t x psi nbsp In Worten Einsetzung von Identischem in Identisches Nutzliche Herleitungen BearbeitenMit den oben aufgestellten Regeln des Sequenzenkalkuls werden nun in endlich vielen Schritten einige weitere nutzliche Regeln hergeleitet Zur Unterscheidung von den obigen Grundregeln heissen sie auch abgeleitete Regeln Zur Erinnerung Herleitung ist gleichzusetzen mit Sequenzenmanipulation durch Anwendung der Regeln Diese einmal abgeleiteten Regeln konnen dann problemlos verwendet werden das heisst es reicht deren Herleitung hier einmal zu zeigen Hier werden folgende Regeln bewiesen der Satz vom ausgeschlossenen Dritten die Trivialitat der Kettenschluss die Kontraposition und der disjunktive Syllogismus Zur Notation Jede Herleitung ist in drei Spalten aufgeteilt In der linken Spalte befindet sich die Nummerierung der einzelnen Modifikationen Sie sind fur eine unmissverstandliche Bezugnahme durch andere Modifikationen nutzlich Die mittlere Spalte enthalt die neue Modifikation mit einer Abfolge von Sequenzen als Ergebnis Die rechte Spalte enthalt die Information wie die Sequenz in der mittleren Spalte erreicht wurde Dabei ist die Regel in Klammern geschrieben und eventuell durch ein Doppelpunkt eingeleitet zu lesen als angewendet auf sind die fur das Ergebnis relevanten Zeilennummern notiert Bsp Ant 1 2 wird gelesen als Antezedensregel angewendet auf Zeile eins und zwei Satz vom ausgeschlossenen Dritten Bearbeiten AD f f displaystyle left text AD right qquad frac varphi vee neg varphi nbsp Herleitung 1 f f Ann 2 f f f Kon1 1 3 f f Ann 4 f f f Kon2 3 5 f f FU 2 4 displaystyle begin alignedat 3 1 quad amp varphi varphi amp quad amp text Ann 2 quad amp varphi varphi vee neg varphi amp quad amp vee text Kon1 1 3 quad amp neg varphi neg varphi amp quad amp text Ann 4 quad amp neg varphi varphi vee neg varphi amp quad amp vee text Kon2 3 5 quad amp varphi vee neg varphi amp quad amp text FU 2 4 end alignedat nbsp Trivialitat Bearbeiten Triv G f G f G ps displaystyle left text Triv right qquad frac begin aligned Gamma varphi Gamma neg varphi end aligned Gamma psi nbsp Herleitung 1 G f Pramisse 2 G f Pramisse 3 G ps f Ant 1 4 G ps f Ant 2 5 G ps KD 3 4 displaystyle begin alignedat 3 1 quad amp Gamma varphi amp quad amp text Pramisse 2 quad amp Gamma neg varphi amp quad amp text Pramisse 3 quad amp Gamma neg psi varphi amp quad amp text Ant 1 4 quad amp Gamma neg psi neg varphi amp quad amp text Ant 2 5 quad amp Gamma psi amp quad amp text KD 3 4 end alignedat nbsp Kettenschluss Bearbeiten KS G f ps G f G ps displaystyle left text KS right qquad frac begin aligned Gamma varphi psi Gamma varphi end aligned Gamma psi nbsp Herleitung 1 G f ps Pramisse 2 G f Pramisse 3 G f f Ant 2 4 G f f Ann 5 G f ps Triv 3 4 6 G ps FU 1 5 displaystyle begin alignedat 3 1 quad amp Gamma varphi psi amp quad amp text Pramisse 2 quad amp Gamma varphi amp quad amp text Pramisse 3 quad amp Gamma neg varphi varphi amp quad amp text Ant 2 4 quad amp Gamma neg varphi neg varphi amp quad amp text Ann 5 quad amp Gamma neg varphi psi amp quad amp text Triv 3 4 6 quad amp Gamma psi amp quad amp text FU 1 5 end alignedat nbsp Anmerkung Bei dieser Herleitung wurde die Regel Triv verwendet An diesem Beispiel sieht man dass eine Regel bloss einmal fehlerfrei hergeleitet zu werden braucht in der Folge kann sie als Abkurzung verwendet werden Durch die Verwendung der Regel Triv wurden funf Herleitungsschritte ausgespart namlich genau die funf Schritte die man benotigt um Triv herzuleiten Kontraposition Bearbeiten KP1 G f ps G ps f displaystyle left text KP1 right qquad frac Gamma varphi psi Gamma neg psi neg varphi nbsp KP2 G f ps G ps f displaystyle left text KP2 right qquad frac Gamma varphi neg psi Gamma psi neg varphi nbsp KP3 G f ps G ps f displaystyle left text KP3 right qquad frac Gamma neg varphi psi Gamma neg psi varphi nbsp KP4 G f ps G ps f displaystyle left text KP4 right qquad frac Gamma neg varphi neg psi Gamma psi varphi nbsp Herleitung von KP1 1 G f ps Pramisse 2 G ps f ps Ant 1 3 G ps f ps Ann 4 G ps f f Triv 2 3 5 G ps f f Ann 6 G ps f FU 4 5 displaystyle begin alignedat 3 1 quad amp Gamma varphi psi amp quad amp text Pramisse 2 quad amp Gamma neg psi varphi psi amp quad amp text Ant 1 3 quad amp Gamma neg psi varphi neg psi amp quad amp text Ann 4 quad amp Gamma neg psi varphi neg varphi amp quad amp text Triv 2 3 5 quad amp Gamma neg psi neg varphi neg varphi amp quad amp text Ann 6 quad amp Gamma neg psi neg varphi amp quad amp text FU 4 5 end alignedat nbsp Die Aussagen KP2 bis KP4 lassen sich analog beweisen Disjunktiver Syllogismus Bearbeiten D S G f ps G f G ps displaystyle left DS right qquad frac begin aligned Gamma varphi vee psi Gamma neg varphi end aligned Gamma psi nbsp Herleitung 1 G f ps Pramisse 2 G f Pramisse 3 G f f Ant 2 4 G f f Ann 5 G f ps Triv 4 3 6 G ps ps Ann 7 G f ps ps Ant 5 6 8 G ps KS 7 1 displaystyle begin alignedat 3 1 quad amp Gamma varphi vee psi amp quad amp text Pramisse 2 quad amp Gamma neg varphi amp quad amp text Pramisse 3 quad amp Gamma varphi neg varphi amp quad amp text Ant 2 4 quad amp Gamma varphi varphi amp quad amp text Ann 5 quad amp Gamma varphi psi amp quad amp text Triv 4 3 6 quad amp Gamma psi psi amp quad amp text Ann 7 quad amp Gamma varphi vee psi psi amp quad amp vee text Ant 5 6 8 quad amp Gamma psi amp quad amp text KS 7 1 end alignedat nbsp Eigenschaften des Sequenzenkalkuls BearbeitenKorrektheit Bearbeiten Der Korrektheitssatz lautet wie folgt Fur alle Formelmengen F displaystyle Phi nbsp und alle Formeln f displaystyle varphi nbsp gilt Wenn F f displaystyle Phi vdash varphi nbsp dann F f displaystyle Phi vDash varphi nbsp Die Korrektheit des Sequenzenkalkuls wird dadurch gezeigt dass fur jede einzelne Regel des Sequenzenkalkuls gezeigt wird dass sie korrekt ist das heisst dass jedes Modell M displaystyle mathfrak M nbsp und jede Variablenbelegung s die die Pramissen der Regel wahr machen auch deren Konsequenz wahr machen Alle Korrektheitsbeweise zusammengenommen ergeben dann den Beweis des Korrektheitssatzes Definitionen Bearbeiten Um den Korrektheitssatz zeigen zu konnen mussen zuvor noch Modell Variablenbelegung und wahr machen logische Wahrheit definiert werden Modell Bearbeiten Ein Modell ist ein geordnetes Paar M D I displaystyle mathfrak M D mathfrak I nbsp sodass gilt D displaystyle D nbsp ist eine nicht leere Menge der Trager oder der Gegenstandsbereich englisch domain uber den die Quantoren laufen I displaystyle mathfrak I nbsp ist die Interpretationsfunktion fur Pradikate Funktionen und Konstanten in der Folge nicht relevant Variablenbelegung Bearbeiten Eine Variablenbelegung s uber einem Modell M D I displaystyle mathfrak M D mathfrak I nbsp ist eine Funktion s v 0 v 1 D displaystyle s v 0 v 1 dots rightarrow D nbsp Logische Wahrheit Folge Bearbeiten Fur alle Formeln f displaystyle varphi nbsp und alle Formelmengen F displaystyle Phi nbsp gilt f displaystyle varphi nbsp folgt logisch aus F displaystyle Phi nbsp kurz F f displaystyle Phi vDash varphi nbsp gdw fur alle Modelle M displaystyle mathfrak M nbsp und alle Variablenbelegungen s uber M displaystyle mathfrak M nbsp gilt Wenn M s F displaystyle mathfrak M s vDash Phi nbsp dann M s f displaystyle mathfrak M s vDash varphi nbsp M a W Jedes M s displaystyle mathfrak M s nbsp das F displaystyle Phi nbsp wahr macht macht auch f displaystyle varphi nbsp wahr Korrektheit der Regeln des Sequenzenkalkuls Bearbeiten Die Korrektheit der Regeln des Sequenzenkalkuls zeigt man indem man die logische Wahrheit der Regeln zeigt Dabei stutzt man sich auf die Definition der logischen Wahrheit Folge Nun wird gezeigt dass jede einzelne Regel des Sequenzenkalkuls logisch wahr ist Es werden nicht alle Beweise gezeigt Es reicht lediglich einige wenige zu skizzieren Die restlichen Beweise sind von der Struktur her ahnlich Korrektheit von Ant Bearbeiten Angenommen G f displaystyle Gamma varphi nbsp ist korrekt d h G f displaystyle Gamma vDash varphi nbsp Sei G displaystyle Gamma nbsp eine Formelmenge sodass gilt G G displaystyle Gamma subseteq Gamma nbsp Seien M s displaystyle mathfrak M s nbsp beliebig gewahlt sodass gilt M s G displaystyle mathfrak M s vDash Gamma nbsp Dann gilt auch M s G displaystyle mathfrak M s vDash Gamma nbsp und laut Voraussetzung auch M s f displaystyle mathfrak M s vDash varphi nbsp Daraus folgt G f displaystyle Gamma vDash varphi nbsp Also ist G f displaystyle Gamma varphi nbsp korrekt Korrektheit von Ann Bearbeiten Wenn f G displaystyle varphi in Gamma nbsp dann gilt G f displaystyle Gamma vDash varphi nbsp Somit ist G f displaystyle Gamma varphi nbsp korrekt Korrektheit von FU Bearbeiten Angenommen G ps f displaystyle Gamma psi varphi nbsp und G ps f displaystyle Gamma neg psi varphi nbsp sind korrekt d h G ps f displaystyle Gamma cup psi vDash varphi nbsp und G ps f displaystyle Gamma cup neg psi vDash varphi nbsp Seien M s displaystyle mathfrak M s nbsp beliebig gewahlt sodass gilt M s G displaystyle mathfrak M s vDash Gamma nbsp Fall 1 M s ps displaystyle mathfrak M s vDash psi nbsp Dann M s G ps displaystyle mathfrak M s vDash Gamma cup psi nbsp und somit nach Voraussetzung M s f displaystyle mathfrak M s vDash varphi nbsp Fall 2 M s ps displaystyle mathfrak M s nvDash psi nbsp Dann M s ps displaystyle mathfrak M s vDash neg psi nbsp Dann M s G ps displaystyle mathfrak M s vDash Gamma cup neg psi nbsp und somit nach Voraussetzung M s f displaystyle mathfrak M s vDash varphi nbsp In beiden Fallen gilt G f displaystyle Gamma vDash varphi nbsp Somit ist G f displaystyle Gamma varphi nbsp korrekt Korrektheit von KD Bearbeiten Angenommen G ps r displaystyle Gamma cup neg psi vDash rho nbsp und G ps r displaystyle Gamma cup neg psi vDash neg rho nbsp Dann gilt fur alle M s displaystyle mathfrak M s nbsp mit M s G ps displaystyle mathfrak M s vDash Gamma cup neg psi nbsp M s r displaystyle mathfrak M s vDash rho nbsp und M s r displaystyle mathfrak M s nvDash rho nbsp Dann gibt es kein M s displaystyle mathfrak M s nbsp sodass gilt M s G ps displaystyle mathfrak M s vDash Gamma cup neg psi nbsp Dann gilt fur alle M s displaystyle mathfrak M s nbsp mit M s ps displaystyle mathfrak M s nvDash psi nbsp M s G displaystyle mathfrak M s nvDash Gamma nbsp Somit gilt G ps displaystyle Gamma vDash psi nbsp und somit ist G ps displaystyle Gamma psi nbsp korrekt Hat man noch zusatzlich die restlichen Regeln bewiesen also deren Korrektheit gezeigt so ist der Korrektheitssatz bewiesen und es kann gesagt werden Ist eine Formel im Sequenzenkalkul herleitbar so ist diese Formel auch logisch wahr Vollstandigkeit Bearbeiten Der Kalkul ist ausserdem auch noch vollstandig Das heisst es gilt Fur alle Formelmengen F displaystyle Phi nbsp und alle Formeln f displaystyle varphi nbsp gilt Wenn F f displaystyle Phi vDash varphi nbsp dann F f displaystyle Phi vdash varphi nbsp Intuitiv bedeutet dies dass alle wahren Sequenzen mit Hilfe der oben angegebenen Regeln hergeleitet werden konnen Beispiele BearbeitenZum Schluss sollen noch zwei Beispiele mit dem Sequenzenkalkul vorgefuhrt werden Beispiel 1 Bearbeiten G f ps G f ps displaystyle frac Gamma varphi psi Gamma varphi rightarrow psi nbsp Herleitung 1 G f ps Pramisse 2 G f f ps Kon 1 3 G f f Ann 4 G f f ps Kon 3 5 G f ps FU 2 4 6 G f ps Umformung displaystyle begin alignedat 3 1 quad amp Gamma varphi psi amp quad amp text Pramisse 2 quad amp Gamma varphi neg varphi vee psi amp quad amp vee text Kon 1 3 quad amp Gamma neg varphi neg varphi amp quad amp text Ann 4 quad amp Gamma neg varphi neg varphi vee psi amp quad amp vee text Kon 3 5 quad amp Gamma neg varphi vee psi amp quad amp text FU 2 4 6 quad amp Gamma varphi rightarrow psi amp quad amp text Umformung end alignedat nbsp Beispiel 2 Bearbeiten G f ps G f displaystyle frac Gamma varphi wedge psi Gamma varphi nbsp Herleitung 1 G f ps Pramisse 2 G f ps Umformung 3 G f f Ann 4 G f f ps Kon 3 5 G f f ps Ant 2 6 G f f Triv 4 5 7 G f f Ann 8 G f FU 7 6 displaystyle begin alignedat 3 1 quad amp Gamma varphi wedge psi amp quad amp text Pramisse 2 quad amp Gamma neg neg varphi vee neg psi amp quad amp text Umformung 3 quad amp Gamma neg varphi neg varphi amp quad amp text Ann 4 quad amp Gamma neg varphi neg varphi vee neg psi amp quad amp vee text Kon 3 5 quad amp Gamma neg varphi neg neg varphi vee neg psi amp quad amp text Ant 2 6 quad amp Gamma neg varphi varphi amp quad amp text Triv 4 5 7 quad amp Gamma varphi varphi amp quad amp text Ann 8 quad amp Gamma varphi amp quad amp text FU 7 6 end alignedat nbsp Literatur BearbeitenHeinz Dieter Ebbinghaus Jorg Flum Wolfgang Thomas Einfuhrung in die mathematische Logik Berlin Springer Verlag 2007 Gerhard Gentzen hrsg M E Szabo The Collected Papers of Gerhard Gentzen Amsterdam 1969 Wolfgang Rautenberg Einfuhrung in die Mathematische Logik Ein Lehrbuch 3 uberarbeitete Auflage Vieweg Teubner Wiesbaden 2008 ISBN 978 3 8348 0578 2 Gaisi Takeuti Proof theory Studies in logic and the foundations of mathematics Band 81 2 Auflage North Holland Amsterdam 1987 ISBN 0 444 87943 9 Richter M M Logikkalkule Stuttgart Teubner Verlag 1978 A S Troelstra H Schwichtenberg Basic Proof Theory Cambridge Tracts in Theoretical Computer Science Cambridge University Press ISBN 0 521 77911 1 Weblinks BearbeitenSequent Calculus by Alex Sakharov MathWorld Jan von Plato The Development of Proof Theory Natural deduction and sequent calculus In Edward N Zalta Hrsg Stanford Encyclopedia of Philosophy Frederic Portoraro Automated Reasoning Sequent Deduction In Edward N Zalta Hrsg Stanford Encyclopedia of Philosophy Abgerufen von https de wikipedia org w index php title Sequenzenkalkul amp oldid 208101232