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. In einem weiteren Sinne kann er als ein System des natürlichen Schließens verstanden werden. Für den Sequenzenkalkül gilt der Vollständigkeitssatz.

Sequenzen und Schlussregeln

Als Sequenz definiert man einen Ausdruck der Form ${\displaystyle \Gamma \Rightarrow \Delta }$, wobei ${\displaystyle \Gamma }$ und ${\displaystyle \Delta }$ endliche Mengen von Formeln sind. Man bezeichnet ${\displaystyle \Gamma }$ mit Antezedens und ${\displaystyle \Delta }$ mit Sukzedens. Eine Sequenz ${\displaystyle \Gamma \Rightarrow \Delta }$ heißt gültig, wenn jedes Modell von ${\displaystyle \Gamma }$ auch Modell mindestens einer Formel aus ${\displaystyle \Delta }$ ist. Eine Belegung, unter der alle Formeln in ${\displaystyle \Gamma }$ wahr werden, aber alle Formeln in ${\displaystyle \Delta }$ falsch werden, falsifiziert die Sequenz.

Beispiel

Die Sequenz ${\displaystyle A,B,C\Rightarrow A\land B,D}$ besagt, dass aus den Aussagen ${\displaystyle A}$, ${\displaystyle B}$ und ${\displaystyle C}$ mindestens eine der Aussagen ${\displaystyle A\land B}$ und ${\displaystyle D}$ folgt.

Das Folgerungszeichen ${\displaystyle \Rightarrow }$ darf nicht verwechselt werden mit der materialen Implikation ${\displaystyle \to }$. Ersteres dient zur Bildung einer Sequenz, während letztere Bestandteil einer Formel ist.

Als Schlussregel bezeichnet man eine Figur der Form

${\displaystyle \left({\text{R}}\right)\qquad {\frac {S_{1},\dots ,S_{n}}{S}}}$

In Klammern steht der Name R der Regel. Die Sequenzen ${\displaystyle S_{1},\dots ,S_{n}}$ heißen Prämissen, die Sequenz ${\displaystyle S}$ heißt die Konklusion der Regel. Eine Schlussregel erlaubt es, aus einer Menge gegebener Sequenzen weitere Sequenzen abzuleiten. Axiome sind Spezialfälle mit ${\displaystyle n=0}$.

Aussagenlogischer Sequenzenkalkül

Im aussagenlogischen Sequenzenkalkül sind als Formeln nur zugelassen. Es gibt ein "strukturelles" Axiom:

${\displaystyle \left({\text{Taut}}\right)\qquad {\frac {-}{\Gamma ,A\Rightarrow A,\Delta }}}$

Für jeden Junktor und jede Seite der Sequenz gibt es (höchstens) eine Schlussregel.

${\displaystyle \left(\bot \Rightarrow \right)\qquad {\frac {-}{\Gamma ,\bot \Rightarrow \Delta }}\qquad \qquad \qquad \left(\Rightarrow \top \right)\qquad {\frac {-}{\Gamma \Rightarrow \Delta ,\top }}}$
(Wenn man die nullstelligen Junktoren ${\displaystyle \bot }$ („falsum“) und ${\displaystyle \top }$ („verum“) verwendet.)

${\displaystyle \left(\neg \Rightarrow \right)\qquad {\frac {\Gamma \Rightarrow \Delta ,F}{\Gamma ,\neg F\Rightarrow \Delta }}\qquad \qquad \qquad \left(\Rightarrow \neg \right)\qquad {\frac {\Gamma ,F\Rightarrow \Delta }{\Gamma \Rightarrow \Delta ,\neg F}}}$

${\displaystyle \left(\vee \Rightarrow \right)\qquad {\frac {\Gamma ,F\Rightarrow \Delta \qquad \Gamma ,G\Rightarrow \Delta }{\Gamma ,F\vee G\Rightarrow \Delta }}\quad \left(\Rightarrow \vee \right)\qquad {\frac {\Gamma \Rightarrow \Delta ,F,G}{\Gamma \Rightarrow \Delta ,F\vee G}}}$

${\displaystyle \left(\wedge \Rightarrow \right)\qquad {\frac {\Gamma ,F,G\Rightarrow \Delta }{\Gamma ,F\wedge G\Rightarrow \Delta }}\qquad \qquad \quad \left(\Rightarrow \wedge \right)\qquad {\frac {\Gamma \Rightarrow \Delta ,F\qquad \Gamma \Rightarrow \Delta ,G}{\Gamma \Rightarrow \Delta ,F\wedge G}}}$

Prädikatenlogischer Sequenzenkalkül

Man erhält den prädikatenlogischen Sequenzenkalkül aus dem aussagenlogischen Sequenzenkalkül, indem man als Formeln auch prädikatenlogische Formeln zulässt und Schlussregeln für die beiden Quantoren hinzufügt. Um die Schlussregeln für die Quantoren auszudrücken, wird die Operation des Einsetzens (der Substitution) benötigt. ${\displaystyle F\left[x/t\right]}$ bezeichnet die Formel, die aus F entsteht, wenn jedes freie Vorkommen der Variablen x durch den Term t ersetzt wird. Ein Vorkommen der Variablen x heißt dabei frei, wenn dieses Vorkommen nicht im Kontext eines Quantors für x steht.

${\displaystyle \left(\exists \Rightarrow \right)\qquad {\frac {\Gamma ,F\left[x/a\right]\Rightarrow \Delta }{\Gamma ,\exists xF\Rightarrow \Delta }}\qquad \qquad \quad \left(\Rightarrow \forall \right)\qquad {\frac {\Gamma \Rightarrow \Delta ,F\left[x/a\right]}{\Gamma \Rightarrow \Delta ,\forall xF}}}$

Hier steht ${\displaystyle a}$ für eine „frische“ Konstante, also eine Konstante, die nicht in ${\displaystyle \Gamma }$, ${\displaystyle \Delta }$ oder ${\displaystyle F}$ vorkommt.

${\displaystyle \left(\Rightarrow \exists \right)\qquad {\frac {\Gamma \Rightarrow \Delta ,F\left[x/t\right]}{\Gamma \Rightarrow \Delta ,\exists xF}}\qquad \qquad \quad \left(\forall \Rightarrow \right)\qquad {\frac {\Gamma ,F\left[x/t\right]\Rightarrow \Delta }{\Gamma ,\forall xF\Rightarrow \Delta }}}$

Hier steht ${\displaystyle t}$ für einen beliebigen Term.

Prädikatenlogischer Sequenzenkalkül mit Gleichheit

${\displaystyle \left(=\right)\qquad {\frac {\Gamma ,t=t\Rightarrow \Delta }{\Gamma \Rightarrow \Delta }}}$

Im Sequenzenkalkül gültige Regeln

Folgende Regeln sind im Sequenzenkalkül gültig:

Mischung

${\displaystyle \left({\text{mix}}\right)\qquad {\frac {\Gamma \Rightarrow M\qquad \Delta \Rightarrow \ B}{\Gamma ,\Delta -M\Rightarrow \ B}}}$

${\displaystyle \Delta -M}$ bezeichnet die Formelfolge, die entsteht, wenn man in ${\displaystyle \Delta }$ jedes vorkommende M streicht.

Schnittregel

${\displaystyle \left({\text{cut}}\right)\qquad {\frac {\Gamma \Rightarrow A\qquad A,\Delta \Rightarrow \ B}{\Gamma ,\Delta \Rightarrow \ B}}}$ (siehe Schnittregel)

Für die Beweisidee siehe Gentzenscher Hauptsatz.

Weblinks

• Alex Sakharov: Sequent Calculus. In: 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.