Benutzer:Dhanyavaada/Sequenzenkalkül

In der Beweistheorie und der mathematischen Logik bezeichnet man mit Sequenzenkalkül eine Familie [[Formales <;System|formaler Systeme]] (oder Kalküle ), die einen bestimmten Stil der Ableitung und gewisse gemeinsame Eigenschaften teilen. Die ersten Sequenzenkalküle, LK für die klassische und LJ für die intuitionistische Logik, sind von Gerhard Gentzen im Jahr 1934 als formaler Rahmen für die Untersucheng von Systeme natürlichen Schliessens in der Prädikatenlogik 1. Ordnung.

Der Gentzensche Hauptsatz über LK und LJ besagt, dass die Schnittregel in diesen Systemen gilt, ein Satz mit weitreichenden Konsequenzen in der Metalogik. Die Flexibilität des Sequenzenkalküls zeigte sich später, im Jahr 1936, als Gentzen die Technik der Schnitt-Elimination verwendete, um die Konsistenz der Peano-Axiome zu beweisen.

Die auf Gentzen zurückgehenden Sequenzenkalküle und die allgemeinen Konzepte, die dahinter stehen, werden in weiten Bereichen der Beweistheorie, mathematischen Logik und des maschinengestützten Beweisens standardmässig verwendet.

Einleitung

Der Sequenzenkalkül dient dazu, das Vorgehen beim mathematischen Beweisen von Theoremen möglichst genau abzubilden. Ein Bestandteil dieser Beweismethode ist, dass an jeder Stelle des Beweises Zusatzvoraussetzungen eingebracht werden können, die dann entweder bis zum Schluss stehen bleiben oder aber wieder eliminiert werden können.

Die Grundeinheit des Sequenzenkalküls ist eine Zeichenfolge (eine Sequenz) aus Variablen $\phi _{i},\phi \!\;$, die jeweils für Ausdrücke des jeweils betrachteten logischen Systems stehen; z.B. für Ausdrücke einer Sprache erster Stufe. Eine solche Sequenz bezeichnen wir mit

$\phi _{1}\phi _{2}...\phi _{n}\phi \!\;$,

oder kürzer mit

$\Gamma \phi \!\;$

,

wobei $\Gamma$ für die Folge der Ausdrücke $\phi _{1},...,\phi _{n}\!\;$ steht. Die Idee dabei ist, dass in $\Gamma \!\;$ die Voraussetzungen stehen und das letzte Glied $\phi$ die Folgerung aus diesen Voraussetzungen bezeichnet.

Der Sequenzenkalkül beschäftigt sich mit der Ableitung von Sequenzen. Gibt es im Kalkül eine Ableitung der Sequenz $\Gamma \phi \!\;$, dann schreibt man auch

$\vdash \Gamma \phi \!\;$

.

Definition: Der Ausdruck $\phi \!\;$ heisst aus $\Phi$ ableitbar (kurz: $\Phi \vdash \phi \!\;$), wenn es $\phi _{1},...,\phi _{n}\!\;$ gibt mit $\vdash \phi _{1},...,\phi _{n},\phi \!\;$.

Die Sequenzenregeln: Allgemeine Gestalt

Im Folgenden führen wir die Regeln für den Sequenzenkalkül der Prädikatenlogik erster Stufe auf, die dem System LK von Gentzen entsprechen. Sequenzenregeln haben dabei die allgemeine Gestalt

${\frac {\Gamma _{1}\phi _{1},\Gamma _{2}\phi _{2},...,\Gamma _{n}\phi _{n}}{\Gamma \phi }}$

Oberhalb des Striches stehen bereits abgeleitete Sequenzen, und unterhalb die daraus ableitbare Sequenz.

Andere Schreibweise

Sequenzenregeln findet man in der Literatur auch in der Form

${\frac {\Gamma _{1}\vdash \phi _{1},\Gamma _{2}\vdash \phi _{2},...,\Gamma _{n}\vdash \phi _{n}}{\Gamma \vdash \phi }}$

oder auch als

${\frac {\Gamma _{1}\Rightarrow \phi _{1},\Gamma _{2}\Rightarrow \phi _{2},...,\Gamma _{n}\Rightarrow \phi _{n}}{\Gamma \Rightarrow \phi }}$

notiert.

Die Grundregeln

Voraussetzungsregel

Diese Regel erlaubt es, an jeder Stelle eines Beweises beliebige Voraussetzungen einzuführen. Dies ist die einzige Regel, in der oberhalb des Querstriches eine leere Sequenz steht:

${\frac {}{\Gamma \phi }}\quad (Vor.)$