Sequenzenkalkül

Grundidee und Sequenzen

Der Sequenzenkalkül, auch Gentzenkalkül, ist ein von Gerhard Gentzen entwickelter logischer Kalkül. Er wurde vor allem für metalogische Zwecke konzipiert, kann aber im weiteren Sinn als System des natürlichen Schließens verstanden werden. Für ihn gilt der Vollständigkeitssatz.

Eine Sequenz hat die Form Γ ⇒ Δ. Γ und Δ sind endliche Mengen von Formeln; Γ heißt Antezedens, Δ heißt Sukzedens. Die Sequenz ist gültig, wenn jedes Modell von Γ auch Modell mindestens einer Formel aus Δ ist. Anders gesagt: Es darf keine Belegung geben, unter der alle Formeln in Γ wahr, aber sämtliche Formeln in Δ falsch sind.

Das Zeichen ⇒ ist kein Bestandteil einer Formel und darf nicht mit der materialen Implikation → verwechselt werden. ⇒ bildet eine Sequenz, → ist dagegen ein Junktor innerhalb einer Formel.

Schlussregeln und Beispiel

Eine Schlussregel hat die Form (R) S₁, …, Sₙ / S. R ist der Name der Regel, S₁ bis Sₙ sind ihre Prämissen und S ist ihre Konklusion. Sie erlaubt, aus gegebenen Sequenzen weitere Sequenzen abzuleiten. Axiome sind der Sonderfall n = 0.

Die Sequenz A, B, C ⇒ A ∧ B, D besagt: Aus A, B und C folgt mindestens eine der Aussagen A ∧ B und D. Dabei muss also nicht jede Formel im Sukzedens folgen.

Aussagenlogische Regeln

Im aussagenlogischen Sequenzenkalkül sind nur aussagenlogische Formeln zugelassen. Das strukturelle Axiom lautet (Taut): Γ, A ⇒ A, Δ.

Für die Junktoren gibt es Regeln für die linke und rechte Seite einer Sequenz. Bei ⊥ darf direkt Γ, ⊥ ⇒ Δ geschlossen werden, bei ⊤ direkt Γ ⇒ Δ, ⊤.

Negation verschiebt eine Formel auf die andere Seite: Aus Γ ⇒ Δ, F folgt Γ, ¬F ⇒ Δ; aus Γ, F ⇒ Δ folgt Γ ⇒ Δ, ¬F.

Für die Disjunktion gilt: Um Γ, F ∨ G ⇒ Δ herzuleiten, müssen sowohl Γ, F ⇒ Δ als auch Γ, G ⇒ Δ gelten. Um Γ ⇒ Δ, F ∨ G herzuleiten, genügt Γ ⇒ Δ, F, G.

Für die Konjunktion gilt umgekehrt: Aus Γ, F, G ⇒ Δ folgt Γ, F ∧ G ⇒ Δ. Für Γ ⇒ Δ, F ∧ G werden beide Prämissen Γ ⇒ Δ, F und Γ ⇒ Δ, G benötigt.

Quantoren und Gleichheit

Der prädikatenlogische Sequenzenkalkül erweitert den aussagenlogischen, indem auch prädikatenlogische Formeln zugelassen und Regeln für Quantoren ergänzt werden. F[x/t] bezeichnet die Formel, die entsteht, wenn jedes freie Vorkommen der Variablen x in F durch den Term t ersetzt wird. Frei bedeutet: Das Vorkommen steht nicht im Kontext eines Quantors für x.

Für Existenzquantor links und Allquantor rechts wird eine frische Konstante a verwendet, die in Γ, Δ und F nicht vorkommt: Aus Γ, F[x/a] ⇒ Δ folgt Γ, ∃xF ⇒ Δ; aus Γ ⇒ Δ, F[x/a] folgt Γ ⇒ Δ, ∀xF.

Für Existenzquantor rechts und Allquantor links darf t ein beliebiger Term sein: Aus Γ ⇒ Δ, F[x/t] folgt Γ ⇒ Δ, ∃xF; aus Γ, F[x/t] ⇒ Δ folgt Γ, ∀xF ⇒ Δ.

Mit Gleichheit kommt die Regel (=) hinzu: Aus Γ, t = t ⇒ Δ folgt Γ ⇒ Δ.

Weitere gültige Regeln

Die Mischungsregel (mix) lautet: Aus Γ ⇒ M und Δ ⇒ B folgt Γ, Δ − M ⇒ B. Δ − M ist die Formelfolge, die entsteht, wenn jedes in Δ vorkommende M gestrichen wird.

Die Schnittregel (cut) lautet: Aus Γ ⇒ A und A, Δ ⇒ B folgt Γ, Δ ⇒ B. Die Beweisidee wird im Zusammenhang mit Gentzens Hauptsatz angegeben.