Sequenzenkalkül

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

In der Beweistheorie und der mathematischen Logik bezeichnet man mit Sequenzenkalkül eine Familie formaler 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:

  • \Gamma ,\Phi …: Formelmengen
  • \varphi , \psi , \rho …: Formeln der Prädikatenlogik
  • \vdash : Zeichen für Herleitungsbeziehung
  • \vDash ,\nvDash : Zeichen für die Beziehung der logischen Wahrheit/Folge
  • \neg : Negationszeichen
  • \vee : Adjunktionszeichen
  • \exists : Existenzquantor
  • (,) : Klammern als Hilfszeichen für mehr Übersichtlichkeit
  • ' : Kennzeichnung für die Erweiterung einer Formelmenge
  • \mathfrak{M} : Zeichen für Modell
  • s : (Zeichen für Variablenbelegungsfunktion)

Es werden folgende Konventionen eingeführt:

  • Mittels diverser Regeln lassen sich die übrigen Junktoren \wedge, \rightarrow,\leftrightarrow in Formeln umformen, die dann nur noch \neg und \vee enthalten. Die Umformungregeln folgen:
    • (\varphi\wedge\psi ):\Leftrightarrow\neg (\neg\varphi\vee\neg\psi )
    • (\varphi\rightarrow\psi ):\Leftrightarrow (\neg\varphi\vee\psi )
    • (\varphi\leftrightarrow\psi ):\Leftrightarrow\neg (\neg(\neg\varphi\vee\psi)\vee\neg(\neg\psi\vee\varphi))
  • Mittels einer Umformungsregel lässt sich der Quantor \forall (Allquantor) wie folgt darstellen:
    • \forall x\varphi:\Leftrightarrow\neg\exists x\neg\varphi

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 \phi_i, \phi\!\;, 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

\phi_1 \phi_2 \dots \phi_n \phi\!\;

oder kürzer mit

\Gamma \phi\!\;,

wobei \Gamma für die Folge der Ausdrücke \phi_1, \dots, \phi_n\!\; steht. Die Idee dabei ist, dass in \Gamma\!\; die Voraussetzungen stehen und das letzte Glied \phi die Folgerung aus diesen Voraussetzungen bezeichnet. Die Voraussetzungen werden auch als Antezedens bezeichnet und die Folgerung als Sukzedens. Während die hier dargestellte Variante des Kalküls der 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 \Gamma \phi \!\;, dann schreibt man auch

\vdash \Gamma \phi\!\;.

Definition: Der Ausdruck \phi\!\; heißt aus \Phi ableitbar (kurz: \Phi \vdash \phi \!\;), wenn es \phi_1, \dots, \phi_n\!\; aus \Phi gibt mit \vdash \phi_1, \dots, \phi_n,\phi \!\;.

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


  \frac{\Gamma_1 \phi_1,\Gamma_2 \phi_2, \dots, \Gamma_n \phi_n}{\Gamma \phi}.

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


  \frac{\Gamma_1 \vdash\phi_1,\Gamma_2 \vdash \phi_2, \dots, \Gamma_n \vdash \phi_n}{\Gamma \vdash \phi}

oder auch als


  \frac{\Gamma_1 \Rightarrow\phi_1,\Gamma_2 \Rightarrow \phi_2, \dots, \Gamma_n \Rightarrow \phi_n}{\Gamma \Rightarrow \phi}

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]

\left(\text{Ant}\right) \qquad \frac{\Gamma\varphi}{\Gamma '\varphi},

wobei gilt: \Gamma\subseteq\Gamma '

In Worten: Man kann problemlos Annahmen hinzufügen.

Annahmeregel[Bearbeiten]

\left(\text{Ann}\right)\qquad\frac{}{\Gamma\varphi}, wobei gilt: \varphi\in\Gamma

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]

\left(\text{FU}\right)\qquad\frac{
\begin{align}
{\Gamma\psi\varphi, \Gamma\neg\psi\varphi}
\end{align}
}
{\Gamma\varphi}

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

Kontradiktion[Bearbeiten]

\left(\text{KD}\right)\qquad\frac{
\begin{align}
{\Gamma\neg\psi\rho, \Gamma\neg\psi\neg\rho}
\end{align}
}
{\Gamma\psi}

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

Adjunktionseinführung im Antezedens[Bearbeiten]

\left(\vee -\text{Ant}\right)\qquad\frac{
\begin{align}
{\Gamma\varphi\rho, \Gamma\psi\rho}
\end{align}
}
{\Gamma (\varphi\vee\psi )\rho}

In Worten: Disjunktionen der Form (\varphi\vee\psi ) im Antezedens können auf zwei Weisen verwendet werden - einerseits im Fall \varphi und andererseits im Fall \psi.

Adjunktionseinführung im Konsequens[Bearbeiten]

\left(\vee -\text{Kon1}\right)\qquad\frac{
\begin{align}
{\Gamma\varphi}
\end{align}
}
{\Gamma (\varphi\vee\psi )}
\quad\left(\vee -\text{Kon2}\right)\qquad\frac{
\begin{align}
{\Gamma\psi}
\end{align}
}
{\Gamma (\varphi\vee\psi )}

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]

\left(\exists -\text{Kon}\right)\qquad\frac{\Gamma\varphi\frac{t}{x}}{\Gamma\exists x\varphi}

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

Existenzeinführung im Antezedens[Bearbeiten]

\left(\exists -\text{Ant}\right)\qquad\frac{\Gamma\varphi\frac{y}{x}\psi}{\Gamma\exists x\varphi\psi}, wenn y in der Sequenz \exists x\varphi\psi nicht frei vorkommt.

Identitätsregeln[Bearbeiten]

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

Reflexivität[Bearbeiten]

\left(\text{Ref}\right) \qquad \frac{}{t\equiv t}

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

Substitutionsregel[Bearbeiten]

\left(\exists -\text{Sub}\right)\qquad\frac{\Gamma\varphi\frac{t}{x}\psi}{\Gamma t\equiv t'\varphi\frac{t'}{x}\psi}

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]

\left(\text{AD}\right)\qquad\frac{}{\varphi\vee\neg\varphi}

Herleitung:


\begin{alignat}{3}
 1.\quad & \varphi\varphi &\quad & (\text{Ann})\\
 2.\quad & \varphi (\varphi\vee\neg\varphi ) &\quad & (\vee -\text{Kon1}):1.\\
 3.\quad & \neg\varphi\neg\varphi &\quad & (\text{Ann})\\
 4.\quad & \neg\varphi (\varphi\vee\neg\varphi ) &\quad & (\vee -\text{Kon2}):3.\\
 5.\quad & (\varphi\vee\neg\varphi ) &\quad & (\text{FU}):2.,4.
\end{alignat}

Trivialität[Bearbeiten]

\left(\text{Triv}\right)\qquad\frac{
\begin{align}
\Gamma\varphi, \Gamma\neg\varphi
\end{align}
}
{\Gamma\psi}

Herleitung:


\begin{alignat}{3}
 1.\quad & \Gamma\varphi &\quad & (\text{Prämisse})\\
 2.\quad & \Gamma\neg\varphi &\quad & (\text{Prämisse})\\
 3.\quad & \Gamma\neg\psi\varphi &\quad & (\text{Ant}):1.\\
 4.\quad & \Gamma\neg\psi\neg\varphi &\quad & (\text{Ant}):2.\\
 5.\quad & \Gamma\psi &\quad & (\text{KD}):3.,4.
\end{alignat}

Kettenschluss[Bearbeiten]

\quad\left(\text{KS}\right)\qquad\frac{
\begin{align}
\Gamma\varphi\psi, \Gamma\varphi
\end{align}
}
{\Gamma\psi}

Herleitung:


\begin{alignat}{3}
 1.\quad & \Gamma\varphi\psi &\quad & (\text{Prämisse})\\
 2.\quad & \Gamma\varphi &\quad & (\text{Prämisse})\\
 3.\quad & \Gamma\neg\varphi\varphi &\quad & (\text{Ant}):2.\\
 4.\quad & \Gamma\neg\varphi\neg\varphi &\quad & (\text{Ann})\\
 5.\quad & \Gamma\neg\varphi\psi &\quad & (\text{Triv}):3.,4.\\
 6.\quad & \Gamma\psi &\quad & (\text{FU}):1.,5.
\end{alignat}

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]

\left(KP1\right)\qquad\frac{
\Gamma\varphi\psi
}
{\Gamma\neg\psi\neg\varphi}


\left(KP2\right)\qquad\frac{
\Gamma\varphi\neg\psi
}
{\Gamma\psi\neg\varphi}


\left(KP3\right)\qquad\frac{
\Gamma\neg\varphi\psi
}
{\Gamma\neg\psi\varphi}


\left(KP4\right)\qquad\frac{
\Gamma\neg\varphi\neg\psi
}
{\Gamma\psi\varphi}

Herleitung von (KP1)((KP2)-(KP4) analog):


\begin{alignat}{3}
 1.\quad & \Gamma\varphi\psi &\quad & (\text{Prämisse})\\
 2.\quad & \Gamma\neg\psi\varphi\psi &\quad & (\text{Ant}):1.\\
 3.\quad & \Gamma\neg\psi\varphi\neg\psi &\quad & (\text{Ann})\\
 4.\quad & \Gamma\neg\psi\varphi\neg\varphi &\quad & (\text{Triv}):2.,3.\\
 5.\quad & \Gamma\neg\psi\neg\varphi\neg\varphi &\quad & (\text{Ann})\\
 6.\quad & \Gamma\neg\psi\neg\varphi &\quad & (\text{FU}):4.,5.
\end{alignat}

Disjunktiver Syllogismus[Bearbeiten]

\left(DS\right)\qquad\frac{
\begin{align}
\Gamma (\varphi\vee\psi ), \Gamma\neg\varphi
\end{align}
}
{\Gamma\psi}

Herleitung:


\begin{alignat}{3}
 1.\quad & \Gamma (\varphi\vee\psi ) &\quad & (\text{Prämisse})\\
 2.\quad & \Gamma\neg\varphi &\quad & (\text{Prämisse})\\
 3.\quad & \Gamma\varphi\neg\varphi &\quad & (\text{Ant}):2.\\
 4.\quad & \Gamma\varphi\varphi &\quad & (\text{Ann})\\
 5.\quad & \Gamma\varphi\psi &\quad & (\text{Triv}):4.,3.\\
 6.\quad & \Gamma\psi\psi &\quad & (\text{Ann})\\
 7.\quad & \Gamma (\varphi\vee\psi )\psi &\quad & (\vee -\text{Ant}):5.,6.\\
 8.\quad & \Gamma\psi &\quad & (\text{KS}):7.,1.
\end{alignat}

Eigenschaften des Sequenzenkalküls[Bearbeiten]

Korrektheit[Bearbeiten]

Der Korrektheitssatz lautet wie folgt:

Für alle Formelmengen \Phi und alle Formeln \varphi gilt: Wenn \Phi\vdash\varphi, dann \Phi\vDash\varphi.

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 \mathfrak{M} 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 \mathfrak{M}=(D,\mathfrak{I} ), sodass gilt:

  1. D ist eine nicht-leere Menge (die "Domäne" oder der "Gegenstandsbereich", über die/den die Quantoren laufen)
  2. \mathfrak{I} ist die Interpretationsfunktion für Prädikate, Funktionen und Konstanten (in der Folge nicht relevant)
Variablenbelegung[Bearbeiten]

Eine Variablenbelegung s über einem Modell \mathfrak{M}=(D,\mathfrak{I} ) ist eine Funktion s:\{v_0,v_1, \dots\}\rightarrow D.

Logische Wahrheit/Folge[Bearbeiten]

Für alle Formeln \varphi und alle Formelmengen \Phi gilt: \varphi folgt logisch aus \Phi (kurz: \Phi\vDash\varphi) gdw für alle Modelle \mathfrak{M} und alle Variablenbelegungen s über \mathfrak{M} gilt: Wenn \mathfrak{M},s\vDash\Phi, dann \mathfrak{M},s\vDash\varphi. (M.a.W.: Wenn es \mathfrak{M},s gibt, welche \Phi wahr machen, wird \varphi vom selben \mathfrak{M},s wahr gemacht.)

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, \Gamma\varphi ist korrekt, d. h. \Gamma\vDash\varphi. Sei \Gamma ' eine Formelmenge, sodass gilt: \Gamma\subseteq\Gamma '. Seien \mathfrak{M},s beliebig gewählt, sodass gilt: \mathfrak{M},s\vDash\Gamma '. Dann gilt auch \mathfrak{M},s\vDash\Gamma und laut Voraussetzung auch \mathfrak{M},s\vDash\varphi . Daraus folgt \Gamma '\vDash\varphi. Also ist \Gamma '\varphi korrekt.

Korrektheit von (Ann)[Bearbeiten]

Wenn \varphi\in\Gamma, dann gilt \Gamma\vDash\varphi. Somit ist \Gamma\varphi korrekt.

Korrektheit von (FU)[Bearbeiten]

Angenommen \Gamma\psi\varphi und \Gamma\neg\psi\varphi sind korrekt, d. h. \Gamma\cup\{\psi\}\vDash\varphi und \Gamma\cup\{\neg\psi\}\vDash\varphi. Seien \mathfrak{M},s beliebig gewählt, sodass gilt: \mathfrak{M},s\vDash\Gamma.

Fall 1: \mathfrak{M},s\vDash\psi. Dann \mathfrak{M},s\vDash\Gamma\cup\{\psi\} und somit nach Voraussetzung \mathfrak{M},s\vDash\varphi.

Fall 2: \mathfrak{M},s\nvDash\psi. Dann \mathfrak{M},s\vDash\neg\psi. Dann \mathfrak{M},s\vDash\Gamma\cup\{\neg\psi\} und somit nach Voraussetzung \mathfrak{M},s\vDash\varphi.

In beiden Fällen gilt \Gamma\vDash\varphi. Somit ist \Gamma\varphi korrekt.

Korrektheit von (KD)[Bearbeiten]

Angenommen \Gamma\cup\{\neg\psi\}\vDash\rho und \Gamma\cup\{\neg\psi\}\vDash\neg\rho. Dann gilt für alle \mathfrak{M},s mit \mathfrak{M},s\vDash\Gamma\cup\{\neg\psi\}:

\mathfrak{M},s\vDash\rho und \mathfrak{M},s\nvDash\rho. Dann gibt es kein \mathfrak{M},s, sodass gilt: \mathfrak{M},s\vDash\Gamma\cup\{\neg\psi\}. Dann gilt für alle \mathfrak{M},s mit \mathfrak{M},s\nvDash\psi: \mathfrak{M},s\nvDash\Gamma. Somit gilt \Gamma\vDash\psi und somit ist \Gamma\psi 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]

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

Für alle Formelmengen \Phi und alle Formeln \varphi gilt: Wenn \Phi\vDash\varphi, dann \Phi\vdash\varphi.

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]

\frac{
\Gamma\varphi\psi
}
{\Gamma\varphi\rightarrow\psi}

Herleitung:


\begin{alignat}{3}
 1.\quad & \Gamma\varphi\psi &\quad & (\text{Prämisse})\\
 2.\quad & \Gamma\varphi (\neg\varphi\vee\psi ) &\quad & (\vee -\text{Kon}):1.\\
 3.\quad & \Gamma\neg\varphi\neg\varphi &\quad & (\text{Ann})\\
 4.\quad & \Gamma\neg\varphi (\neg\varphi\vee\psi ) &\quad & (\vee -\text{Kon}):3.\\
 5.\quad & \Gamma (\neg\varphi\vee\psi ) &\quad  & (\text{FU}):2.,4.\\
 6.\quad & \Gamma (\varphi\rightarrow\psi ) &\quad & (\text{Umformung}).
\end{alignat}

Beispiel 2[Bearbeiten]

\frac{
\Gamma\varphi\wedge\psi
}
{\Gamma\varphi}

Herleitung:


\begin{alignat}{3}
 1.\quad & \Gamma\varphi\wedge\psi &\quad & (\text{Prämisse})\\
 2.\quad & \Gamma\neg (\neg\varphi\vee\neg\psi ) &\quad & (\text{Umformung})\\
 3.\quad & \Gamma\neg\varphi\neg\varphi &\quad & (\text{Ann})\\
 4.\quad & \Gamma\neg\varphi (\neg\varphi\vee\neg\psi ) &\quad & (\vee -\text{Kon}):3.\\
 5.\quad & \Gamma\neg\varphi\neg(\neg\varphi\vee\neg\psi ) &\quad & (\text{Ant}):2.\\
 6.\quad & \Gamma\neg\varphi\varphi &\quad & (\text{Triv}):4.,5..\\
 7.\quad & \Gamma\varphi\varphi &\quad & (\text{Ann})\\
 8.\quad & \Gamma\varphi &\quad & (\text{FU}):7.,6.
\end{alignat}

Literatur[Bearbeiten]

Weblinks[Bearbeiten]