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 , 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
oder kürzer mit
,
wobei für die Folge der Ausdrücke steht. Die Idee dabei ist, dass in die Voraussetzungen stehen und das letzte Glied 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 , dann schreibt man auch
.
Definition: Der Ausdruck heisst aus ableitbar (kurz: ), wenn es gibt mit .
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
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
oder auch als
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: