Sequenzenkalkül

Methodik der Beweistheorie der Mathematik und der Programmanalyse der Informatik
(Weitergeleitet von Gentzenkalkül)

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

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

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

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
 

Im Sequenzenkalkül gültige Regeln

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.

Bearbeiten