Sequenzenkalkül

Der Sequenzenkalkü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.

Inhaltsverzeichnis

1 Aussagenlogischer Sequenzenkalkül

1.1 Schlussregeln

2 Prädikatenlogischer Sequenzenkalkül

2.1 Schlussregeln

3 Prädikatenlogischer Sequenzenkalkül mit Gleichheit

Aussagenlogischer Sequenzenkalkül

Eine aussagenlogische Sequenz ist ein Ausdruck der Form $\Gamma \Rightarrow \Delta$ , wobei $Γ,Δ$ endliche Mengen von aussagenlogischen Formeln sind. Man bezeichnet $Γ$ mit Antezedens und $Δ$ mit Sukzedens. Eine Sequenz $\Gamma \Rightarrow \Delta$ heißt gültig, wenn jedes Modell von $Γ$ auch Modell mindestens einer Formel aus $Δ$ ist. Gibt es eine Belegung, unter der alle Formeln in $Γ$ wahr werden, aber alle Formeln in $Δ$ falsch werden, so falsifiziert eine derartige Belegung die Sequenz.

Schlussregeln

Die Sequenzen der ersten Zeile heißen Prämissen, die der zweiten Zeile Konklusion.

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

$\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 \wedge G}$

$\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

Eine prädikatenlogische Sequenz ist ein Ausdruck der Form $\Gamma \Rightarrow \Delta$ , wobei $Γ,Δ$ endliche Mengen von geschlossenen prädikatenlogischen Formeln sind. Man bezeichnet $Γ$ mit Antezedens und $Δ$ mit Sukzedens. Eine Sequenz $\Gamma \Rightarrow \Delta$ heißt gültig, wenn jedes Modell von $Γ$ auch Modell mindestens einer Formel aus $Δ$ ist, d.h. wenn $\bigwedge\Gamma\models\bigvee\Delta$ . Gibt es eine Struktur, unter der alle Formeln in $Γ$ wahr werden, aber alle Formeln in $Δ$ falsch werden, so falsifiziert eine derartige Struktur die Sequenz.

Schlussregeln

Die Sequenzen der ersten Zeile heißen Prämissen, die der zweiten Zeile Konklusion.

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

$\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 \wedge G}$

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

$\left(\exists\Rightarrow\right)\qquad\frac{\Gamma,F\left[x/a\right]\Rightarrow\Delta}{\Gamma,\exists xF\Rightarrow\Delta}$ , $a$ darf nicht in $Γ$ , $Δ$ oder $F [x]$ vorkommen.

$\left(\Rightarrow\forall \right)\qquad\frac{\Gamma\Rightarrow\Delta, F\left[x/a\right]}{\Gamma\Rightarrow\Delta,\forall xF}$ , $a$ darf nicht in $Γ$ , $Δ$ oder $F [x]$ vorkommen.

Prädikatenlogischer Sequenzenkalkül mit Gleichheit

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

Sequenzenkalkül

Aussagenlogischer Sequenzenkalkül

Schlussregeln

Prädikatenlogischer Sequenzenkalkül

Schlussregeln

Prädikatenlogischer Sequenzenkalkül mit Gleichheit

See also: Sequenzenkalkül, Antezedens, Aussagenlogik, Gerhard Gentzen, Konklusion, Logik, Metalogik, Modell, Prämisse, Sukzedens