Baumkalkül

Elemente der Logik durch indirekten Beweis, indem sie die Umöglichkeit des Gegenteils belegen
(Weitergeleitet von Tableaukalkül)

Baumkalküle oder Tableaukalküle, nach ihrem Erfinder auch Beth-Kalküle genannt, sind Widerlegungskalküle der Logik.

Der Name Baumkalkül rührt daher, dass beim Ableiten in einem Beth-Kalkül eine Baumstruktur erzeugt wird. Diese Aussage ist eine Beschreibung, keine Definition, weil nicht jeder Kalkül, der Baumstrukturen erzeugt, auch Baumkalkül genannt wird. Die entstandenen Baumstrukturen werden auch Beth-Tableaux oder Beth-Tableaus (französischer bzw. eingedeutschter Plural von Beth-Tableau) genannt.

Grundlagen

Bearbeiten

Für klassische Logiken lässt sich intuitiv ein semantischer Schlussbegriff fassen: Ein Argument ist genau dann gültig, wenn unter allen Interpretationen, unter denen alle Prämissen wahr sind, auch die Konklusion wahr ist; kürzer, prägnanter und mit Leibniz: Aus Wahrem folgt nur Wahres. Somit ist ein Argument genau dann ungültig, wenn es mindestens eine Interpretation gibt, unter der alle Prämissen wahr sind, die Konklusion aber falsch ist.

Wenn ein Satz falsch ist, dann ist nach der klassischen Semantik seine Verneinung wahr. Statt zu sagen, ein Argument ist genau dann ungültig, wenn es mindestens eine Interpretation gibt, unter der alle Prämissen wahr sind, unter der die Konklusion aber falsch ist, kann man daher genauso gut folgendes sagen: Ein Argument ist genau dann ungültig, wenn es mindestens eine Interpretation gibt, unter der alle Prämissen wahr sind und unter der auch die Negation der Konklusion wahr ist.

Kürzer: Ein Argument  , wobei   die Menge der Prämissen,   die Konklusion ist und das metalogische Zeichen   die Gültigkeit des Arguments aussagt, ist genau dann ungültig, wenn es mindestens eine Interpretation I gibt, unter der jeder Satz aus   wahr ist, unter der   aber falsch ist. Da nach der Semantik der Negation I( ) = F genau dann, wenn I( ) = W, ist   genau dann ungültig, wenn I nicht nur jeden Satz aus  , sondern auch   wahr macht, wenn also I jeden Satz aus der Menge   wahr macht. Ein Argument   ist also genau dann ungültig, wenn die Menge   erfüllbar ist, und im Umkehrschluss genau dann gültig, wenn die Menge   unerfüllbar bzw. inkonsistent ist.

Beth-Kalküle versuchen, die Gültigkeit eines Arguments zu widerlegen (auch deshalb „Widerlegungskalkül“), indem sie den Vorgang formalisieren, ein Modell für   anzugeben. So sind die Formationsregeln des Kalküls rein syntaktisch und können ohne jeden semantischen Hintergedanken angewendet werden, sind aber, indem sie letztlich die Gegenmodellkonstruktion formalisieren, semantisch motiviert.

Modelle konstruieren

Bearbeiten

Im ersten Schritt soll überlegt werden, wie man für die einzelnen Arten von Aussagen ein Modell bildet. Dabei soll eine aussagenlogische Sprache zugrunde gelegt werden, deren Junktoren folgende sind:   (Negation),   (Konjunktion),   (Disjunktion, nichtausschließendes Oder) und   (Konditional oder materiale Implikation). Die Negation verneint den Wahrheitswert eines Satzes; eine Konjunktion verbindet zwei Sätze zu einem neuen Satz, der genau dann wahr ist, wenn beide verbundenen Sätze wahr sind, und der andernfalls falsch ist; die Disjunktion verbindet zwei Sätze zu einem neuen Satz, der nur dann falsch ist, wenn beide verbundenen Sätze falsch sind, und der andernfalls wahr ist; und das Konditional verbindet zwei Sätze zu einem neuen Satz, der nur dann falsch ist, wenn der linke der beiden verbundenen Sätze wahr und der rechte falsch ist.

  • Am einfachsten lässt sich ein Modell für einen atomaren Satz   konstruieren: Man setzt   und hat in   ein geeignetes Modell.
  • Nicht viel schwieriger ist es, ein Modell für   zu konstruieren (dabei darf anstelle von   auch ein beliebig komplexer zusammengesetzter Satz stehen): Man setzt   und hat in   ein geeignetes Modell.
  • Auch ein Modell für   ist rasch erzeugt: Man setzt   und hat per Wahrheitsdefinition der Konjunktion mit   in   ein Modell für  .
  • Um ein Modell für   zu erzeugen, gibt es drei Möglichkeiten: (a) Man setzt  , (b) man setzt  , oder (c) man macht beides.
  • Auch die Konstruktion eines Modells für   lässt mehrere Möglichkeiten zu: (a) Man setzt  ; (b) man setzt  ; (c) man macht beides.

Nach diesen Möglichkeiten sind die Transformationsregeln des Beth-Kalküls modelliert.

Ein erster Blick auf den Kalkül

Bearbeiten

Im Ausgang werden alle Sätze der Menge   untereinander aufgeschrieben. Dies wird am Beispiel des Arguments   gezeigt. Bei diesem Argument ist   und ist  , ist also  .   ist hier  , also  . Man schreibt somit:

a.  
b.  
c.  

Die Reihenfolge ist, da es sich um eine Satzmenge handelt, gleichgültig. Diese Satzmenge wird als Knoten – als ein Knoten – eines Baums angesehen, deshalb die Umrahmung. Nun wird versucht, für diese Satzmenge ein Modell zu bilden, also jeden Satz dieser Menge wahr zu machen. Im Fall der Sätze b. und c. ist das einfach: Damit eine Interpretation   ein Modell für b. ist, muss   sein. Damit   ein Modell für c. ist, muss   sein. Damit hat man erste Informationen über  .

Schwieriger ist es mit Satz a. Dieser Satz ist ein Konditional, es gibt also drei Möglichkeiten, ihn zu erfüllen: (a)  , (b)   und (c) beides. Man schreibt die Möglichkeiten (a) und (b) als Kinder des Baums auf; Möglichkeit (c) braucht man nicht gesondert anzuschreiben, weil sie die Kombination von (a) und (b) bedeutet. Um anzuzeigen, dass man Satz a. damit abgehandelt hat, wird er – je nach Geschmack – durchgestrichen, abgehakt oder ganz entfernt. Es entsteht in diesem Schritt folgender Baum:

a.  
b.  
c.  
d.  
e.  

Dabei liest sich Knoten bzw. Satz d. wie folgt: „Zusätzlich zu den nicht durchgestrichenen Anforderungen, die meine Vorfahren an   stellen, stelle ich an   die Anforderung, dass  .“ (Diese Anforderung resultierte aus der Behandlung von Satz a.)

Knoten bzw. Satz e. liest sich wie folgt: „Zusätzlich zu den nicht durchgestrichenen Anforderungen, die meine Vorfahren an   stellen, stelle ich an   die Anforderung, dass  .“

Man sieht, dass Knoten d. eine unerfüllbare Anforderung an   stellt: Der Knoten fordert auf Grund von Satz d., dass   ist. Zugleich erbt er aber von seinem Vater auf Grund von Satz b. die Forderung, dass   ist. Da diese beiden Forderungen nicht vereinbar sind, ist der linke Versuch, ein Modell für   zu bilden, frühzeitig gescheitert. Man markiert das im Baum auf geeignete Weise:

a.  
b.  
c.  
d.  
e.  

Man liest das als: „Der linke Zweig ist geschlossen“.

Der rechte Zweig ist noch offen und damit die Hoffnung, ein Modell zu finden, noch nicht verloren. Wann ist   ein Modell für  ? Auf Grund der Wahrheitswertdefinitionen der Konjunktion genau dann, wenn  . Das schreibt man auf und streicht den damit abgehandelten Satz e.:

a.  
b.  
c.  
d.  
e.  
f.  
g.  

Jetzt liest sich Knoten e. wie folgt: „Zusätzlich zu den Anforderungen, die mein Vater an   richtet, fordere ich von  , dass   und dass  .“

Der Weg, der von der Wurzel zu Knoten e. führt, enthält nur mehr atomare Sätze. Die Anforderungen an ein Modell von   können daher direkt abgelesen werden: Damit   ein solches Modell ist, muss es folgende Anforderungen erfüllen:

  1. aus b. I(P) = W
  2. aus c. I(Q) = F
  3. aus f. I(Q) = W
  4. aus g. I(R) = W

Forderungen b. und g. sind unproblematisch, aber Forderungen c. und f. widersprechen einander und sind daher unerfüllbar. Damit ist es auch im zweiten Ast des Baums nicht gelungen, ein Modell für   zu bilden. Der Ast ist also ebenfalls geschlossen, sein Endknoten wird markiert:

a.  
b.  
c.  
d.  
e.  
f.  
g.  

Da keine weiteren Äste mehr vorhanden und alle vorhandenen Äste geschlossen sind, wird der ganze Baum geschlossen genannt. Die Geschlossenheit des Baums zeigt an, dass es unmöglich ist, ein Modell für   zu bilden. Das wiederum bedeutet, dass es unmöglich ist, das Argument   zu widerlegen. Somit ist das Argument   damit bewiesen.

Schlussregeln des aussagenlogischen Baumkalküls

Bearbeiten
Und-Regel
Tritt in einem Knoten eine Aussage   auf, wird diese durchgestrichen und der Knoten wird um die beiden Sätze   und   erweitert.
Oder-Regel
Tritt in einem Knoten eine Aussage   auf, wird diese durchgestrichen und der Knoten erhält zwei Kinder. Eines der beiden Kinder enthält den Satz  , das andere Kind enthält den Satz  .
Pfeil-Regel
Tritt in einem Knoten eine Aussage   auf, wird diese durchgestrichen und der Knoten erhält zwei Kinder. Eines der beiden Kinder enthält den Satz  , das andere Kind enthält den Satz  .
Nicht-Und-Regel
Tritt in einem Knoten eine Aussage   auf, wird diese durchgestrichen und der Knoten erhält zwei Kinder. Eines der beiden Kinder enthält den Satz  , das andere Kind enthält den Satz  .
Nicht-Oder-Regel
Tritt in einem Knoten eine Aussage   auf, wird diese durchgestrichen und der Knoten wird um den Satz   und um den Satz   erweitert.
Nicht-Pfeil-Regel
Tritt in einem Knoten eine Aussage   auf, wird diese durchgestrichen und der Knoten wird um den Satz   und um den Satz   erweitert.

Diese Regeln müssen so lange auf den Baum angewendet werden, bis alle nichtatomaren Sätze durchgestrichen sind. Der entstandene Baum heißt genau dann geschlossen, wenn jeder direkte Weg von der Wurzel bis zu einem Endknoten mindestens einen Widerspruch enthält. Ein Weg enthält genau dann einen Widerspruch, wenn er sowohl einen Satz   als auch dessen Negation   enthält.

Ist der Baum nicht geschlossen, d. h. gibt es mindestens einen widerspruchsfreien direkten Weg von der Wurzel bis zu einem Endknoten, dann heißt der Baum offen.

Das Argument, für das der Baum gebildet wurde, ist genau dann gültig, wenn der Baum geschlossen ist. Das Argument ist genau dann ungültig, wenn der Baum offen ist. In diesem Fall lässt sich an jedem offenen Ast ein Gegenbeispiel für das Argument ablesen.

Der Beth-Kalkül für die klassische Aussagenlogik, so wie er hier aufgestellt wurde, ist korrekt und vollständig, und er ist ein Entscheidungsverfahren für die klassisch-aussagenlogische Gültigkeit von Argumenten.

Literatur

Bearbeiten
  • Evert Willem Beth: Semantic Entailment and formal derivability. In: Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Band 18, Nummer 13, Amsterdam 1955, S. 309–342, gekürzter, übersetzter Nachdruck in Berka/Kreiser 1986, S. 262 ff.
    Erste systematische Ausarbeitung des Baumkalküls
  • Evert Willem Beth: A topological proof of the theorem of Löwenheim-Skolem-Gödel. In: Indag. Math., 13, S. 346–344
    Erste Gedanken in Richtung eines Baumkalküls
  • Karel Berka, Lothar Kreiser: Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik. Akademie, Berlin 1986
    Gekürzter, übersetzter Nachdruck von Beth 1955 ab S. 262

Sekundärliteratur

Bearbeiten
  • Ansgar Beckermann: Einführung in die Logik. 3. Auflage. De Gruyter, Berlin 2010, ISBN 978-3-11-025434-1.
    In dieser Einführung wird ein Baumkalkül für Aussagen- und Prädikatenlogik von Grund auf und auf einem für Anfänger verständlichen Niveau entwickelt.
  • Wilfrid Hodges: Logic. 2. Auflage. Penguin, London 2001, ISBN 0-14-100314-6 (englisch)
    Ein sehr einfach beginnendes Einführungsbuch in die formale Logik, in dem langsam ein Baumkalkül entwickelt wird. Für Einsteiger in die formale Logik, die der englischen Sprache mächtig sind, wäre es eine ausgezeichnete Wahl.
  • Wolfgang Bibel: Deduktion. Automatisierung der Logik (=Handbuch der Informatik 6.2). Oldenbourg, München 1992, ISBN 3-486-20785-7
    Der Titel steht stellvertretend für Werke, deren Zielsetzung innerhalb der Informatik und im automatisierten Beweisen liegt, einer Zielsetzung, bei der überwiegend mit Widerlegungskalkülen gearbeitet wird. Voraussetzung für das fruchtbare Studium solcher Titel sind Vorkenntnisse auf dem Gebiet der formalen Logik und der Programmierung.
Bearbeiten