Gentzenkalkül

Der Sequenzenkalkül (manchmal auch Gentzenkalkül) ist ein von Gerhard Gentzen entwickelter, primär für metalogische Zwecke konzipierter logischer Kalkül.

Notationen und Konventionen

In diesem Artikel werden folgende Zeichen verwendet:

• Γ,Φ ... (Formelmengen)
• $\varphi , \psi , \rho$ ... (Formeln)
• $\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.

Definition

Eine Sequenz ist eine endliche Abfolge von Formeln, formal <$\varphi_1\varphi_2...\varphi_n$, wobei $\varphi_1\varphi_2...\varphi_{n-1}$ das Antezedens und $\varphi_n$ das Konsequens ist. Γ,Δ,... seien Variablen für Sequenzen.

Sei Φ eine Formelmenge und $\varphi$ eine Formel. $\varphi$ ist aus Φ herleitbar (kurz: $\Phi\vdash \varphi$ ) :gdw (genau dann wenn) es $\varphi_1 ,...,\varphi_n \in\Phi$ gibt, sodass $\varphi_1 ...\varphi_n\varphi$ im Sequenzenkalkül herleitbar ist. (M.a.W.: Mittels Regeln werden die Sequenzen so lange manipuliert, bis man das gewünschte Ergebnis erhält.)

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

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

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

Antezedensregel

$\quad\left(Ant\right)\qquad\frac{\Gamma\varphi}{\Gamma '\varphi}$ wobei gilt: $\Gamma\subseteq\Gamma '$.

In Worten: Man kann problemlos Annahmen hinzufügen.

Annahmeregel

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

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

Junktorenregeln

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

Fallunterscheidung

$\quad\left(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 ψ und andererseits unter der Annahme von $\neg\psi$ herleiten kann, darf man, ohne irgendeine Annahme über ψ oder $\neg\psi$ machen zu müssen, auf $\varphi$ schließen.

Kontradiktion

$\quad\left(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 ψ geschlossen werden.

Adjunktionseinführung im Antezedens

$\quad\left(\vee -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 ψ.

Adjunktionseinführung im Konsequens

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

$\quad\left(\vee -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

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

Existenzeinführung im Konsequens

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

In Worten: Wenn man aus Γ 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

$\quad\left(\exists -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

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

Reflexivität

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

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

Substitutionsregel

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

In Worten: Einsetzung von Identischem in Identisches.

Nützliche Herleitungen

Mit den oben aufgestellten Regeln des Sequenzenkalküls werden nun in endlichen Schritten einige nützliche Gesetze hergeleitet. (Zur Erinnerung: Herleitung ist gleichzusetzen mit Sequenzenmanipulation durch Anwendung der Regeln.) Diese Gesetze können dann problemlos verwendet werden, das heißt es reicht, deren Herleitung hier einmal zu zeigen. Hier werden folgende Gesetze gezeigt: 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

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

Herleitung:

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

Trivialität

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

Herleitung:

$\begin{alignat}{3} 1.\quad &amp;amp; \Gamma\varphi &amp;amp;\quad &amp;amp; (Praemisse)\\ 2.\quad &amp;amp; \Gamma\neg\varphi &amp;amp;\quad &amp;amp; (Praemisse)\\ 3.\quad &amp;amp; \Gamma\neg\psi\varphi &amp;amp;\quad &amp;amp; (Ant):1.\\ 4.\quad &amp;amp; \Gamma\neg\psi\neg\varphi &amp;amp;\quad &amp;amp; (Ant):2.\\ 5.\quad &amp;amp; \Gamma\psi &amp;amp;\quad &amp;amp; (KD):3.,4. \end{alignat}$

Kettenschluss

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

Herleitung:

$\begin{alignat}{3} 1.\quad &amp;amp; \Gamma\varphi\psi &amp;amp;\quad &amp;amp; (Praemisse)\\ 2.\quad &amp;amp; \Gamma\varphi &amp;amp;\quad &amp;amp; (Praemisse)\\ 3.\quad &amp;amp; \Gamma\neg\varphi\varphi &amp;amp;\quad &amp;amp; (Ant):2.\\ 4.\quad &amp;amp; \Gamma\neg\varphi\neg\varphi &amp;amp;\quad &amp;amp; (Ann)\\ 5.\quad &amp;amp; \Gamma\neg\varphi\neg\psi &amp;amp;\quad &amp;amp; (Triv):3.,4.\\ 6.\quad &amp;amp; \Gamma\psi &amp;amp;\quad &amp;amp; (FU):1.,5. \end{alignat}$

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

Kontraposition

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

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

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

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

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

$\begin{alignat}{3} 1.\quad &amp;amp; \Gamma\varphi\psi &amp;amp;\quad &amp;amp; (Praemisse)\\ 2.\quad &amp;amp; \Gamma\neg\psi\varphi\psi &amp;amp;\quad &amp;amp; (Ant):1.\\ 3.\quad &amp;amp; \Gamma\neg\psi\varphi\neg\psi &amp;amp;\quad &amp;amp; (Ann)\\ 4.\quad &amp;amp; \Gamma\neg\psi\varphi\neg\varphi &amp;amp;\quad &amp;amp; (Triv):2.,3.\\ 5.\quad &amp;amp; \Gamma\neg\psi\neg\varphi\neg\varphi &amp;amp;\quad &amp;amp; (Ann)\\ 6.\quad &amp;amp; \Gamma\neg\psi\neg\varphi &amp;amp;\quad &amp;amp; (FU):4.,5. \end{alignat}$

Disjunktiver Syllogismus

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

Herleitung:

$\begin{alignat}{3} 1.\quad &amp;amp; \Gamma (\varphi\vee\psi ) &amp;amp;\quad &amp;amp; (Praemisse)\\ 2.\quad &amp;amp; \Gamma\neg\varphi &amp;amp;\quad &amp;amp; (Praemisse)\\ 3.\quad &amp;amp; \Gamma\varphi\neg\varphi &amp;amp;\quad &amp;amp; (Ant):2.\\ 4.\quad &amp;amp; \Gamma\varphi\varphi &amp;amp;\quad &amp;amp; (Ann)\\ 5.\quad &amp;amp; \Gamma\varphi\psi &amp;amp;\quad &amp;amp; (Triv):4.,3.\\ 6.\quad &amp;amp; \Gamma\psi\psi &amp;amp;\quad &amp;amp; (Ann)\\ 7.\quad &amp;amp; \Gamma (\varphi\vee\psi )\psi &amp;amp;\quad &amp;amp; (\vee -Ant):5.,6.\\ 8.\quad &amp;amp; \Gamma\psi &amp;amp;\quad &amp;amp; (KS):7.,1. \end{alignat}$

Eigenschaften des Sequenzenkalküls

Korrektheit

Der Korrektheitssatz lautet wie folgt:

Für alle Formelmengen Φ 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, d.h., dass ein Modell $\mathfrak{M}$ und eine Variablenbelegung s existieren, die die Regel wahr machen. Alle Korrektheitsbeweise zusammengenommen ergeben dann den Beweis des Korrektheitssatzes.

Definitionen

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

Modell

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

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

Logische Wahrheit/Folge

Für alle Formeln $\varphi$ und alle Formelmengen Φ gilt: $\varphi$ folgt logisch aus Φ (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 Φ wahrmachen, wird $\varphi$ vom selben $\mathfrak{M},s$ wahr gemacht.)

Korrektheit der Regeln des Sequenzenkalküls

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 Beiweise gezeigt. Es reicht lediglich einige wenige zu skizzieren. Die restlichen Beweise sind von der Struktur her ähnlich.)

Korrektheit von (Ant)

Angenommen, $\Gamma\varphi$ ist korrekt, d.h. $\Gamma\vDash\varphi$. Sei Γ' 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)

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

Korrektheit von (FU)

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}\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)

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\Gamma$: $\mathfrak{M},s\nvDash\psi$. Somit gilt $\Gamma\vDash\psi$ 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

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

Für alle Formelmengen Φ 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

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

Beispiel 1

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

Herleitung:

$\begin{alignat}{3} 1.\quad &amp;amp; \Gamma\varphi\psi &amp;amp;\quad &amp;amp; (Praemisse)\\ 2.\quad &amp;amp; \Gamma\varphi (\neg\varphi\vee\psi ) &amp;amp;\quad &amp;amp; (\vee -Kon):1.\\ 3.\quad &amp;amp; \Gamma\neg\varphi\neg\varphi &amp;amp;\quad &amp;amp; (Ann)\\ 4.\quad &amp;amp; \Gamma\neg\varphi (\neg\varphi\vee\psi ) &amp;amp;\quad &amp;amp; (\vee -Kon):3.\\ 5.\quad &amp;amp; \Gamma (\neg\varphi\vee\psi ) &amp;amp;\quad &amp;amp; (FU):2.,4.\\ 6.\quad &amp;amp; \Gamma (\varphi\rightarrow\psi ) &amp;amp;\quad &amp;amp; (Umformung). \end{alignat}$

Beispiel 2

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

Herleitung:

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

Literatur

• Ebbinghaus H.-D., Flum J., Thomas W.: Einführung in die mathematische Logik. Berlin: Springer-Verlag, 2007.
• Richter, M. M.: Logikkalküle. Stuttgart: Teubner Verlag, 1978.

Weblinks

• Sequent Calculus by Alex Sakharov MathWorld
• Jan von Plato: „The Development of Proof Theory: Natural deduction and sequent calculus“ in der Stanford Encyclopedia of Philosophy (englisch, inklusive Literaturangaben)
• Frederic Portoraro: „Automated Reasoning: Sequent Deduction“ in der Stanford Encyclopedia of Philosophy (englisch, inklusive Literaturangaben)