Tableaukalkül

Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth-Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments beweisen, sondern die dessen Ungültigkeit widerlegen; ein anderer, sehr bekannter Widerlegungskalkül ist der Resolutionskalkül.

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.

In diesem Artikel soll ein Baumkalkül für die klassische Aussagenlogik vorgestellt werden: Ein Kalkül für die klassische Logik deshalb, weil die historisch ersten Baumkalküle klassisch waren; ein Kalkül für die Aussagenlogik deshalb, weil dieser der einfachste ist und die Grundlage vieler anderer Baumkalküle bildet, zunächst für den Baumkalkül der wichtigen klassischen Prädikatenlogik. Tableaukalküle gibt es auch für viele nichtklassische logische Systeme.

Grundlagen

Für klassische Logiken lässt sich sehr 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, unter der 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 $\Gamma \models \varphi$, wobei Γ die Menge der Prämissen, $\varphi$ die Konklusion ist und das metalogische Zeichen $\models$ 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 $\varphi$ aber falsch ist. Da nach der Semantik der Negation I($\varphi$) = F genau dann, wenn I($\neg \varphi$) = W, ist $\Gamma \models \varphi$ genau dann ungültig, wenn I nicht nur jeden Satz aus Γ, sondern auch $\neg \varphi$ wahr macht, wenn also I jeden Satz aus der Menge $\Gamma \cup \{\neg \varphi\}$ wahr macht. Ein Argument $\Gamma \models \varphi$ ist also genau dann ungültig, wenn die Menge $\Gamma \cup \{\neg \varphi\}$ erfüllbar ist, und im Umkehrschluss genau dann gültig, wenn die Menge $\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 $\Gamma \cup \{\neg \varphi\}$ anzugeben. So sind die Formationsregeln des Kalküls zwar rein syntaktisch und können ohne jeden semantischen Hintergedanken angewendet werden, sind aber, indem sie letztlich die Gegenmodellkonstruktion formalisieren, hochgradig semantisch motiviert.

Modelle konstruieren

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 P konstruieren: Man setzt I(P) = W und hat in I ein geeignetes Modell.

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

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

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

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

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

Ein erster Blick auf den Kalkül

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

a. $P \rightarrow (Q \and R)$ b. P c. $\neg Q$

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

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

	a. $P \rightarrow (Q \and R)$ b. P c. $\neg Q$
d. $\neg P$		e. $Q \and R$

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

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

	a. $P \rightarrow (Q \and R)$ b. P c. $\neg Q$
d. $\neg P$		e. $Q \and R$

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

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

	a. $P \rightarrow (Q \and R)$ b. P c. $\neg Q$
d. $\neg P$		e. $Q \and R$ f. Q g. R

Jetzt liest sich Knoten e. wie folgt: „Zusätzlich zu den Anforderungen, die mein Vater an I richtet, fordere ich von I, dass I(Q) = W und dass 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 $\{P \rightarrow (Q \and R), P, \neg Q\}$ können daher direkt abgelesen werden: Damit 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 $\{P \rightarrow (Q \and R), P, \neg Q\}$ zu bilden. Der Ast ist also ebenfalls geschlossen, sein Endknoten wird markiert:

	a. $P \rightarrow (Q \and R)$ b. P c. $\neg Q$
d. $\neg P$		e. $Q \and R$ f. Q g. R

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

Schlussregeln des aussagenlogischen Baumkalküls

Und-Regel

Tritt in einem Knoten eine Aussage P ∧ Q auf, wird diese durchgestrichen und wird der Knoten um die beiden Sätze P und Q erweitert.

Oder-Regel

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

Pfeil-Regel

Tritt in einem Knoten eine Aussage P → Q auf, wird diese durchgestrichen und erhält der Knoten zwei Kinder. Eines der beiden Kinder enthält den Satz ¬P, das andere Kind enthält den Satz Q.

Nicht-Und-Regel

Tritt in einem Knoten eine Aussage ¬(P ∧ Q) auf, wird diese durchgestrichen und erhält der Knoten zwei Kinder. Eines der beiden Kinder enthält den Satz ¬P, das andere Kind enthält den Satz ¬Q.

Nicht-Oder-Regel

Tritt in einem Knoten eine Aussage ¬(P ∨ Q) auf, wird diese durchgestrichen und wird der Knoten um den Satz ¬P und um den Satz ¬Q erweitert.

Nicht-Pfeil-Regel

Tritt in einem Knoten eine Aussage ¬(P → Q) auf, wird diese durchgestrichen und wird der Knoten um den Satz P und um den Satz ¬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 P als auch dessen Negation ¬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 – aber das ist schon eine semantische Interpretation – 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

Primärquellen

• Evert Willem Beth: Semantic Entailment and formal derivability, Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, Band 18, Nummer 13, Amsterdam: 1955, Seite 309-342, gekürzter, übersetzter Nachdruck in Berka/Kreiser 1986, Seite 262 ff.

Erste systematische Ausarbeitung des Baumkalküls

• Evert Willem Beth: A topological proof of the theorem of Löwenheim-Skolem-Gödel, Indag. Math. 13, Seite 346-344

Erste Gedanken in Richtung eines Baumkalküls

• Karel Berka, Lothar Kreiser: Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik, Berlin: Akademie 1986

Gekürzter, übersetzter Nachdruck von Beth 1955 ab Seite 262

Sekundärliteratur

• Wilfrid Hodges ([1]): Logic, London: Penguin ²2001 ISBN 0-141-003-146 in englischer Sprache

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, München: Oldenbourg 1992 (=Handbuch der Informatik 6.2) 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.