Moderne Termlogik: Der Kalkül der Termlogik: Die Transformationsregeln
Moderne Termlogik Bearbeiten
Der Kalkül der Termlogik Bearbeiten
Die Transformationsregeln Bearbeiten
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 Ixy bzw. Axy,Ayz 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:
- Beispiel: Aus den Annahmen können wir mit Hilfe dieser Regeln z.B. die Folgerung ableiten, und zwar wie folgt:
- Aus wird abgeleitet nach R2
- Aus wird abgeleitet nach R4
In diesem Fall schreiben wir ; das Ableitungssymbol wird im folgenden Abschnitt präzise definiert.
