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.

Aussagenlogischer Sequenzenkalkül

Eine aussagenlogische Sequenz ist ein Ausdruck der Form $\Gamma \Rightarrow \Delta$ ,wobei $\Gamma ,\Delta$ endliche Mengen von aussagenlogischen Formeln sind. Man bezeichnet $\Gamma$ mit Antezedens und $\Delta$ mit Sukzedens. Eine Sequenz $\Gamma \Rightarrow \Delta$ heisst gültig, wenn jedes Modell von $\Gamma$ auch Modell mindestens einer Formel aus $\Delta$ ist. Gibt es eine Belegung unter der alle Formeln in $\Gamma$ wahr werden, aber alle Formeln in $\Delta$ 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 $\Gamma ,\Delta$ endliche Mengen von geschlossenen prädikatenlogischen Formeln sind. Man bezeichnet $\Gamma$ mit Antezedenz und $\Delta$ mit Sukzedenz. Eine Sequenz $\Gamma \Rightarrow \Delta$ heisst gültig, wenn jedes Modell von $\Gamma$, das zu $\Delta$ auch Modell mindestens einer Formel aus $\Delta$ ist. Gibt es eine Struktur, unter der alle Formeln in $\Gamma$ wahr werden, aber alle Formeln in $\Delta$ 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 $\Gamma$ oder $\Delta$ vorkommen
  
  

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