Baumkalkü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.

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 ${\displaystyle \Gamma \models \varphi }$, wobei ${\displaystyle \Gamma }$ die Menge der Prämissen, ${\displaystyle \varphi }$ die Konklusion ist und das metalogische Zeichen ${\displaystyle \models }$ die Gültigkeit des Arguments aussagt, ist genau dann ungültig, wenn es mindestens eine Interpretation I gibt, unter der jeder Satz aus ${\displaystyle \Gamma }$ wahr ist, unter der ${\displaystyle \varphi }$ aber falsch ist. Da nach der Semantik der Negation I(${\displaystyle \varphi }$) = F genau dann, wenn I(${\displaystyle \neg \varphi }$) = W, ist ${\displaystyle \Gamma \models \varphi }$ genau dann ungültig, wenn I nicht nur jeden Satz aus ${\displaystyle \Gamma }$, sondern auch ${\displaystyle \neg \varphi }$ wahr macht, wenn also I jeden Satz aus der Menge ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ wahr macht. Ein Argument ${\displaystyle \Gamma \models \varphi }$ ist also genau dann ungültig, wenn die Menge ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ erfüllbar ist, und im Umkehrschluss genau dann gültig, wenn die Menge ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ 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 ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ 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.

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: ${\displaystyle \neg }$ (Negation), ${\displaystyle \land }$ (Konjunktion), ${\displaystyle \vee }$ (Disjunktion, nichtausschließendes Oder) und ${\displaystyle \to }$ (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 ${\displaystyle P}$ konstruieren: Man setzt ${\displaystyle I(P)=W}$ und hat in ${\displaystyle I}$ ein geeignetes Modell.

• Nicht viel schwieriger ist es, ein Modell für ${\displaystyle \neg P}$ zu konstruieren (dabei darf anstelle von ${\displaystyle P}$ auch ein beliebig komplexer zusammengesetzter Satz stehen): Man setzt ${\displaystyle I(P)=F}$ und hat in ${\displaystyle I}$ ein geeignetes Modell.

• Auch ein Modell für ${\displaystyle P\land Q}$ ist rasch erzeugt: Man setzt ${\displaystyle I(P)=I(Q)=W}$ und hat per Wahrheitsdefinition der Konjunktion mit ${\displaystyle I(P\land Q)=W}$ in ${\displaystyle I}$ ein Modell für ${\displaystyle P\land Q}$.

• Um ein Modell für ${\displaystyle P\vee Q}$ zu erzeugen, gibt es drei Möglichkeiten: (a) Man setzt ${\displaystyle I(P)=W}$, (b) man setzt ${\displaystyle I(Q)=W}$, oder (c) man macht beides.

• Auch die Konstruktion eines Modells für ${\displaystyle P\to Q}$ lässt mehrere Möglichkeiten zu: (a) Man setzt ${\displaystyle I(P)=F}$; (b) man setzt ${\displaystyle I(Q)=W}$; (c) man macht beides.

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

Im Ausgang werden alle Sätze der Menge ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ untereinander aufgeschrieben. Dies wird am Beispiel des Arguments ${\displaystyle P\rightarrow (Q\land R),P\models Q}$ gezeigt. Bei diesem Argument ist ${\displaystyle \Gamma =\{P\rightarrow (Q\land R),P\}}$ und ist ${\displaystyle \varphi =Q}$, ist also ${\displaystyle \neg \varphi =\neg Q}$. ${\displaystyle \Gamma \cup \{\neg \varphi \}}$ ist hier ${\displaystyle \{P\rightarrow (Q\land R),P\}\cup \{\neg Q\}}$, also ${\displaystyle \{P\rightarrow (Q\land R),P,\neg Q\}}$. Man schreibt somit:

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 ${\displaystyle I}$ ein Modell für b. ist, muss ${\displaystyle I(P)=W}$ sein. Damit ${\displaystyle I}$ ein Modell für c. ist, muss ${\displaystyle I(Q)=F}$ sein. Damit hat man erste Informationen über ${\displaystyle I}$.

Schwieriger ist es mit Satz a. Dieser Satz ist ein Konditional, es gibt also drei Möglichkeiten, ihn zu erfüllen: (a) ${\displaystyle I(P)=F}$, (b) ${\displaystyle I(Q\land R)=W}$ 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:

Dabei liest sich Knoten bzw. Satz d. wie folgt: „Zusätzlich zu den nicht durchgestrichenen Anforderungen, die meine Vorfahren an ${\displaystyle I}$ stellen, stelle ich an ${\displaystyle I}$ die Anforderung, dass ${\displaystyle I(P)=F}$.“ (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 ${\displaystyle I}$ stellen, stelle ich an ${\displaystyle I}$ die Anforderung, dass ${\displaystyle I(Q\land R)=W}$.“

Man sieht, dass Knoten d. eine unerfüllbare Anforderung an ${\displaystyle I}$ stellt: Der Knoten fordert auf Grund von Satz d., dass ${\displaystyle I(P)=F}$ ist. Zugleich erbt er aber von seinem Vater auf Grund von Satz b. die Forderung, dass ${\displaystyle I(P)=W}$ ist. Da diese beiden Forderungen nicht vereinbar sind, ist der linke Versuch, ein Modell für ${\displaystyle \{P\rightarrow (Q\land R),P,\neg Q\}}$ zu bilden, frühzeitig gescheitert. Man markiert das im Baum auf geeignete Weise:

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 ${\displaystyle I}$ ein Modell für ${\displaystyle Q\land R}$? Auf Grund der Wahrheitswertdefinitionen der Konjunktion genau dann, wenn ${\displaystyle I(Q)=I(R)=W}$. Das schreibt man auf und streicht den damit abgehandelten Satz e.:

Jetzt liest sich Knoten e. wie folgt: „Zusätzlich zu den Anforderungen, die mein Vater an ${\displaystyle I}$ richtet, fordere ich von ${\displaystyle I}$, dass ${\displaystyle I(Q)=W}$ und dass ${\displaystyle I(R)=W}$.“

Der Weg, der von der Wurzel zu Knoten e. führt, enthält nur mehr atomare Sätze. Die Anforderungen an ein Modell von ${\displaystyle \{P\rightarrow (Q\land R),P,\neg Q\}}$ können daher direkt abgelesen werden: Damit ${\displaystyle I}$ 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 ${\displaystyle \{P\rightarrow (Q\land R),P,\neg Q\}}$ zu bilden. Der Ast ist also ebenfalls geschlossen, sein Endknoten wird markiert:

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 ${\displaystyle \{P\rightarrow (Q\land R),P,\neg Q\}}$ zu bilden. Das wiederum bedeutet, dass es unmöglich ist, das Argument ${\displaystyle P\rightarrow (Q\land R),P\models Q}$ zu widerlegen. Somit ist das Argument ${\displaystyle P\rightarrow (Q\land R),P\models Q}$ damit bewiesen.

Und-Regel

Tritt in einem Knoten eine Aussage ${\displaystyle P\land Q}$ auf, wird diese durchgestrichen und der Knoten wird um die beiden Sätze ${\displaystyle P}$ und ${\displaystyle Q}$ erweitert.

Oder-Regel

Tritt in einem Knoten eine Aussage ${\displaystyle P\vee Q}$ auf, wird diese durchgestrichen und der Knoten erhält zwei Kinder. Eines der beiden Kinder enthält den Satz ${\displaystyle P}$, das andere Kind enthält den Satz ${\displaystyle Q}$.

Pfeil-Regel

Tritt in einem Knoten eine Aussage ${\displaystyle P\to Q}$ auf, wird diese durchgestrichen und der Knoten erhält zwei Kinder. Eines der beiden Kinder enthält den Satz ${\displaystyle \neg P}$, das andere Kind enthält den Satz ${\displaystyle Q}$.

Nicht-Und-Regel

Tritt in einem Knoten eine Aussage ${\displaystyle \neg (P\land Q)}$ auf, wird diese durchgestrichen und der Knoten erhält zwei Kinder. Eines der beiden Kinder enthält den Satz ${\displaystyle \neg P}$, das andere Kind enthält den Satz ${\displaystyle \neg Q}$.

Nicht-Oder-Regel

Tritt in einem Knoten eine Aussage ${\displaystyle \neg (P\vee Q)}$ auf, wird diese durchgestrichen und der Knoten wird um den Satz ${\displaystyle \neg P}$ und um den Satz ${\displaystyle \neg Q}$ erweitert.

Nicht-Pfeil-Regel

Tritt in einem Knoten eine Aussage ${\displaystyle \neg (P\to Q)}$ auf, wird diese durchgestrichen und der Knoten wird um den Satz ${\displaystyle P}$ und um den Satz ${\displaystyle \neg Q}$ 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 ${\displaystyle P}$ als auch dessen Negation ${\displaystyle \neg P}$ 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.

• 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

• 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.

• Torsten Wilholt: Logik und Argumentation. (PDF; 2,7 MB) Skript zur Einführung in die formale Logik unter Verwendung eines Baumkalküls für Aussagen- und Prädikatenlogik mit Identität; enthält Beweise für Korrektheit und Vollständigkeit des Kalküls
• Wolfgang Schwarz: Tree Proof Generator. JavaScript, das für logisch wahre Sätze der Aussagen- oder Prädikatenlogik Beweise im Baumkalkül generiert.