Sequenzenkalkül

aus Wikipedia, der freien Enzyklopädie
(Weitergeleitet von Gentzenkalkül)
Zur Navigation springen Zur Suche springen

Der Sequenzenkalkül (manchmal auch Gentzenkalkü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. Für den Sequenzenkalkül gilt der Vollständigkeitssatz.

Sequenzen und Schlussregeln

[Bearbeiten | Quelltext bearbeiten]

Als Sequenz definiert man einen Ausdruck der Form , wobei und endliche Mengen von Formeln sind. Man bezeichnet mit Antezedens und mit Sukzedens. Eine Sequenz heißt gültig, wenn jedes Modell von auch Modell mindestens einer Formel aus ist. Eine Belegung, unter der alle Formeln in wahr werden, aber alle Formeln in falsch werden, falsifiziert die Sequenz.

Beispiel
Die Sequenz besagt, dass aus den Aussagen , und mindestens eine der Aussagen und folgt.

Das Folgerungszeichen darf nicht verwechselt werden mit der materialen Implikation . Ersteres dient zur Bildung einer Sequenz, während letztere Bestandteil einer Formel ist.

Als Schlussregel bezeichnet man eine Figur der Form

In Klammern steht der Name R der Regel. Die Sequenzen heißen Prämissen, die Sequenz heißt die Konklusion der Regel. Eine Schlussregel erlaubt es, aus einer Menge gegebener Sequenzen weitere Sequenzen abzuleiten. Axiome sind Spezialfälle mit .

Aussagenlogischer Sequenzenkalkül

[Bearbeiten | Quelltext bearbeiten]

Im aussagenlogischen Sequenzenkalkül sind als Formeln nur aussagenlogische Formeln zugelassen. Es gibt ein "strukturelles" Axiom:

Für jeden Junktor und jede Seite der Sequenz gibt es (höchstens) eine Schlussregel.


(Wenn man die nullstelligen Junktoren („falsum“) und („verum“) verwendet.)

Prädikatenlogischer Sequenzenkalkül

[Bearbeiten | Quelltext bearbeiten]

Man erhält den prädikatenlogischen Sequenzenkalkül aus dem aussagenlogischen Sequenzenkalkül, indem man als Formeln auch prädikatenlogische Formeln zulässt und Schlussregeln für die beiden Quantoren hinzufügt. Um die Schlussregeln für die Quantoren auszudrücken, wird die Operation des Einsetzens (der Substitution) benötigt. bezeichnet die Formel, die aus F entsteht, wenn jedes freie Vorkommen der Variablen x durch den Term t ersetzt wird. Ein Vorkommen der Variablen x heißt dabei frei, wenn dieses Vorkommen nicht im Kontext eines Quantors für x steht.

Hier steht für eine „frische“ Konstante, also eine Konstante, die nicht in , oder vorkommt.

Hier steht für einen beliebigen Term.

Prädikatenlogischer Sequenzenkalkül mit Gleichheit

[Bearbeiten | Quelltext bearbeiten]

Im Sequenzenkalkül gültige Regeln

[Bearbeiten | Quelltext bearbeiten]

Folgende Regeln sind im Sequenzenkalkül gültig:

Mischung

bezeichnet die Formelfolge, die entsteht, wenn man in jedes vorkommende M streicht.

Schnittregel
(siehe Schnittregel)

Für die Beweisidee siehe Gentzenscher Hauptsatz.