Moderne Termlogik: Der Kalkül der Termlogik: Die Transformationsregeln

Moderne Termlogik

Der Kalkül der Termlogik

Die Transformationsregeln

Die Transformationsregeln des Kalküls der Termlogik dienen dazu, aus einer Anzahl von zugrundegelegten Urteilen, den Annahmen, neue Urteile zu erzeugen. Eine der wichtigsten Regeln der Termlogik, die wir gleich behandeln werden, erlaubt es z.B., aus der Annahme Aab die Folgerung Iba zu erzeugen; eine andere, aus den beiden Annahmen Aab und Abc die Folgerung Aac zu ziehen.

Die Regeln des Kalküls sind Vorschriften, die den Umgang mit Zeichenfolgen betreffen. Eine inhaltliche Interpretation dieser Vorgänge kann nützlich zur Motivation und zum Erinnern sein, die Regeln müssen aber unabhängig davon so beschrieben werden, dass sie als blosse Zeichenmanipulationen von jedem verständigen (und gutwilligen!) Menschen oder von einem Computerprogramm durchgeführt werden können.

Da die Regeln also Handlungsanweisungen sind, muss man sich entscheiden, in welcher Art und Weise man sie notiert und anderen Menschen verständlich zu machen versucht. Wenn man dafür keine Computersprache verwenden will (was mitunter die einfachste Möglichkeit ist), kann man auf die Pfeilnotation zurückgreifen, die man für die Darstellung von Termersetzungssystemen verwendet..

• Beispiel: Die oben angeführten Regeln der Termlogik schreibt man in der Gestalt Axy $\longrightarrow$ Ixy bzw. Axy,Ayz $\longrightarrow$ Axz. Was man damit ausdrücken will, ist das Folgende: Wenn sich unter den Annahmen bzw. den bisher bereits hergeleiteten Urteilen das Urteil Aab befindet, dann "gilt" auch Iab, d.h. das Urteil Iab kann zur Sammlung aus Annahmen und abgeleiteten Urteilen hinzugefügt werden. Genauso kann man nach der zweiten Regel Aac "ableiten", wenn unter den Annahmen bzw. den bereits abgeleiteten Urteilen Aab sowie Abc vorhanden sind. Die Termvariablen x, y, z "stehen für" beliebige Termkonstanten.

Nun werden alle die zur Termlogik gehörenden Transformationsregeln angegeben:

${\begin{array}{ccccl}R1:&Axy&\longrightarrow &Iyx&(partielleA-Konversion,A-pKonv)\\R2:&Exy&\longrightarrow &Eyx&(E-Konversion,E-Konv)\\R3:&Axy,Ayz&\longrightarrow &Axz&(Barbara)\\R4:&Axy,Eyz&\longrightarrow &Exz&(Celarent)\end{array}}$

• Beispiel: Aus den Annahmen ${Aab,Ecb}$ können wir mit Hilfe dieser Regeln z.B. die Folgerung $Eac$ ableiten, und zwar wie folgt:
• Aus $Ecb$ wird $Ebc$ abgeleitet nach R2
• Aus $Aab,Ebc$ wird $Eac$ abgeleitet nach R4

In diesem Fall schreiben wir $Aab,Ecb\vdash Eac$; das Ableitungssymbol $\vdash$ wird im folgenden Abschnitt präzise definiert.