Sequenzenkalkül

Der Sequenzenkalkül ist ein System des natürlichen Schließens, der Logik.

aussagenlogischer Sequenzenkalkül

Eine aussagenlogische Sequenz ist ein Ausdruck der Form $\Gamma \Rightarrow \Delta$ mit $\Gamma ,\Delta$ seien endliche Mengen von aussagenlogischen Formeln. Man bezeichnet $\Gamma$ mit Antezedenz und $\Delta$ mit Sukzedenz. 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 heissen 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 }}$

prädikatenlogischer Sequenzenkalkül

Eine prädikatenlogische Sequenz ist ein Ausdruck der Form $\Gamma \Rightarrow \Delta$ mit $\Gamma ,\Delta$ seien endliche Mengen von geschlossenen prädikatenlogischen Formeln. 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.