Sequenzenkalkül

Sequenzenregeln findet man in der Literatur auch in der Form

${\displaystyle {\frac {\Gamma _{1}\vdash \phi _{1},\Gamma _{2}\vdash \phi _{2},\dots ,\Gamma _{n}\vdash \phi _{n}}{\Gamma \vdash \phi }}}$

oder auch als

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \phi _{1},\Gamma _{2}\Rightarrow \phi _{2},\dots ,\Gamma _{n}\Rightarrow \phi _{n}}{\Gamma \Rightarrow \phi }}}$

notiert.

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

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

wobei gilt: ${\displaystyle \Gamma \subseteq \Gamma '}$

In Worten: Man kann problemlos Annahmen hinzufügen.

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

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

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

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

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

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

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

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

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

${\displaystyle \left(\vee -{\text{Kon1}}\right)\qquad {\frac {\begin{aligned}{\Gamma \varphi }\end{aligned}}{\Gamma (\varphi \vee \psi )}}}$

${\displaystyle \left(\vee -{\text{Kon2}}\right)\qquad {\frac {\begin{aligned}{\Gamma \psi }\end{aligned}}{\Gamma (\varphi \vee \psi )}}}$

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

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

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

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

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

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

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

In Worten: Die Äquivalenzrelation auf dem Gegenstandsbereich ${\displaystyle D}$ ist reflexiv.

${\displaystyle \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.

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

Herleitung:

${\displaystyle {\begin{alignedat}{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{alignedat}}}$

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

Herleitung:

${\displaystyle {\begin{alignedat}{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{alignedat}}}$

${\displaystyle \left({\text{KS}}\right)\qquad {\frac {\begin{aligned}\Gamma \varphi \psi ,\Gamma \varphi \end{aligned}}{\Gamma \psi }}}$

Herleitung:

${\displaystyle {\begin{alignedat}{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{alignedat}}}$

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).

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

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

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

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

Herleitung von (KP1):

${\displaystyle {\begin{alignedat}{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{alignedat}}}$

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

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

Herleitung:

${\displaystyle {\begin{alignedat}{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{alignedat}}}$

Der Korrektheitssatz lautet wie folgt:

Für alle Formelmengen ${\displaystyle \Phi }$ und alle Formeln ${\displaystyle \varphi }$ gilt: Wenn ${\displaystyle \Phi \vdash \varphi }$, dann ${\displaystyle \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 ${\displaystyle {\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.

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

Ein Modell ist ein geordnetes Paar ${\displaystyle {\mathfrak {M}}=(D,{\mathfrak {I}})}$, sodass gilt:

1. ${\displaystyle D}$ ist eine nicht-leere Menge (der Träger oder der Gegenstandsbereich, englisch domain, über den die Quantoren laufen)
2. ${\displaystyle {\mathfrak {I}}}$ ist die Interpretationsfunktion für Prädikate, Funktionen und Konstanten (in der Folge nicht relevant)

Eine Variablenbelegung s über einem Modell ${\displaystyle {\mathfrak {M}}=(D,{\mathfrak {I}})}$ ist eine Funktion ${\displaystyle s:\{v_{0},v_{1},\dots \}\rightarrow D}$.

Für alle Formeln ${\displaystyle \varphi }$ und alle Formelmengen ${\displaystyle \Phi }$ gilt: ${\displaystyle \varphi }$ folgt logisch aus ${\displaystyle \Phi }$ (kurz: ${\displaystyle \Phi \vDash \varphi }$) gdw für alle Modelle ${\displaystyle {\mathfrak {M}}}$ und alle Variablenbelegungen s über ${\displaystyle {\mathfrak {M}}}$ gilt: Wenn ${\displaystyle {\mathfrak {M}},s\vDash \Phi }$, dann ${\displaystyle {\mathfrak {M}},s\vDash \varphi }$. (M.a.W.: Jedes ${\displaystyle {\mathfrak {M}},s}$, das ${\displaystyle \Phi }$ wahr macht, macht auch ${\displaystyle \varphi }$ wahr.)

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.)

Angenommen, ${\displaystyle \Gamma \varphi }$ ist korrekt, d. h. ${\displaystyle \Gamma \vDash \varphi }$. Sei ${\displaystyle \Gamma '}$ eine Formelmenge, sodass gilt: ${\displaystyle \Gamma \subseteq \Gamma '}$. Seien ${\displaystyle {\mathfrak {M}},s}$ beliebig gewählt, sodass gilt: ${\displaystyle {\mathfrak {M}},s\vDash \Gamma '}$. Dann gilt auch ${\displaystyle {\mathfrak {M}},s\vDash \Gamma }$ und laut Voraussetzung auch ${\displaystyle {\mathfrak {M}},s\vDash \varphi }$. Daraus folgt ${\displaystyle \Gamma '\vDash \varphi }$. Also ist ${\displaystyle \Gamma '\varphi }$ korrekt.

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

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

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

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

In beiden Fällen gilt ${\displaystyle \Gamma \vDash \varphi }$. Somit ist ${\displaystyle \Gamma \varphi }$ korrekt.

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

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

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

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

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

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

Herleitung:

${\displaystyle {\begin{alignedat}{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{alignedat}}}$

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

Herleitung:

${\displaystyle {\begin{alignedat}{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{alignedat}}}$