Prädikatenlogik/Erste Stufe/Identität/Syntaktische Tautologien/Sequenzenkalkül ableitbar/Textabschnitt

Gegeben sei ein Symbolalphabet einer Sprache erster Stufe und damit die zugehörige Termmenge und die zugehörige Ausdrucksmenge. Wir möchten die logisch wahren Aussagen einer solchen Sprache syntaktisch charakterisieren. Mathematische Aussagen sind im Allgemeinen „wenn-dann“-Aussagen, d.h. sie behaupten, dass, wenn gewisse Voraussetzungen erfüllt sind, dann auch eine gewisse Folgerung erfüllt ist.

Wenn man einen Beweis eines Satzes der Gruppentheorie oder der elementaren Arithmetik entwirft, so sind dabei die Axiome der Gruppentheorie bzw. die Peano-Axiome stets präsent. Ebenso, wenn man (in einer Theorie) eine Aussage der Form „ ${}p$ impliziert ${}q$ “ beweist, so steht ${}p$ als Annahme zur Verfügung. Von daher ist der zu entwickelnde Kalkül so aufgebaut, dass das Grundschema die Form

$\varphi _{1}\ldots \varphi _{n}\psi$

besitzt (dabei sind ${}\varphi _{1},\ldots ,\varphi _{n}$ und ${}\psi$ Ausdrücke) mit der Bedeutung, dass aus den Voraussetzungen ${}\varphi _{1},\ldots ,\varphi _{n}$ zusammengenommen der Ausdruck ${}\psi$ folgt. Eine solches Grundschema heißt eine Sequenz. Anders als bei der Definition der Ausdrücke sind nur logische gültige Sequenzen erlaubt, und es geht eben darum, all diese gültigen Sequenzen zu generieren. Dies geschieht wiederum rekursiv, und man braucht Anfangssequenzen und Schlussregeln, wie man aus bereits etablierten Sequenzen neue Sequenzen erhält.

Um weiter Schreibarbeit zu sparen, fasst man die ${}n$ Voraussetzungen in einer Sequenz in eine Menge von Aussagen zusammen, die wir mit großen griechischen Buchstaben bezeichnen werden. Das Grundschema hat dann die Gestalt

$\Gamma \psi .$

Häufig wird eine Grundmenge an Voraussetzungen mit geschleppt, aber einzelne weitere Voraussetzungen spielen in einer bestimmten Regel eine aktive Rolle. Dann verwendet man Schreibweisen wie

$\Gamma \varphi \psi ,$

die besagen, dass die Voraussetzungsmenge ${}\Gamma$ zusammen mit der Voraussetzung ${}\varphi$ den Ausdruck ${}\psi$ impliziert. Der Sequenzenkalkül ist ein rein syntaktischer Kalkül, der allerdings versucht, das natürliche Schließen im Rahmen eines mathematischen Beweises nachzubilden. Von daher trägt auch ein Großteil der folgenden Regeln eine Bezeichnung, die aus der Beweispraxis bekannt ist.

Die Sequenz ${}\Gamma q$ wird als

$\vdash p_{1}\land \cdots \land p_{n}\rightarrow q$

interpretiert, wobei die ${}p_{i}$ zu ${}\Gamma$ gehören.

Antezedenzregel

Aus

$\vdash p_{1}\land \cdots \land p_{n}\rightarrow q$

folgt

$\vdash p_{1}\land \cdots \land p_{n}\land p_{n+1}\cdots \land p_{n+m}\rightarrow q.$

Dies ergibt sich im Prädikatenkalkül aus der Transitivitätsregel, Modus ponens und der Konjunktionsregel.

Voraussetzungsregel

Aus Konjunktionsregel.