Moderne Termlogik: Der Kalkül der Termlogik: Direkte Ableitungen
Der Kalkül der Termlogik
[Bearbeiten]Direkte Ableitungen
[Bearbeiten]Wie im vorherigen Abschnitt beschrieben, bedeutet "Direkte Ableitung von Folgerungen aus einer Menge von Annahmen" das Folgende.
Definition:
- Gegeben eine Menge von Urteilen, die Annahmen (oder Voraussetzungen).
- Eine endliche Folge (Sequenz) von Urteilen heisst "Direkte Ableitung von aus ", wenn
- eine Teilmenge von ist
- alle Elemente, die nach kommen (d.h., in der Sequenz rechts von stehen) entweder Wiederholungen von Elementen aus sind oder aus vorhergehenden Elementen durch eine der Regeln erzeugt werden.
Sei eine direkte Ableitung aus . Dann schreiben wir
Diesen Vorgang der Ableitung eines Urteils aus einer Urteilsmenge protokolliert man am einfachsten so ( wir zeigen das an einem Beispiel):
Auf die letzten beiden Spalten kann man auch verzichten, wenn es einem nur auf das Endergebnis, die letzte Zeile ankommt. An unserem Beispiel können wir ablesen, dass die folgende Ableitungsbeziehung gilt:
Folgerung: Aus der Definition der direkten Ableitung folgt unmittelbar, dass für alle Urteile
für alle beliebigen und
gilt; denn ist eine gültige Ableitung (die Wiederholung von ist zulässig nach der obigen Definition).
Diese Tatsache hat grosse Konsequenzen für das gesamte Logiksystem, wie sich im Abschnitt über die indirekte Ableitung zeigen wird: Sie garantiert, dass - wie bei der Aussagenlogik - aus einem Widerspruch jeder beliebige Satz folgt ( ist eine Tautologie). Ein System, in dem das nicht der Fall ist (solche Systeme nennt man parakonsistent) erhält man, wenn man in der obigen Definition der direkten Ableitung die Worte
entweder Wiederholungen von Elementen aus sind oder
streicht. Wir gehen später, im Abschnitt Parakonsistenz, genauer darauf ein.