Beweise und semantische Tableaus

1. Was ein Beweis ist

Ein Argument ist die Behauptung, dass eine Konklusion aus bestimmten Prämissen folgt. Ein Beweis ist das, was diese Behauptung entscheidet: ein endliches, überprüfbares Gebilde, das jeder Zeile für Zeile nachlesen und bestätigen kann, ohne Ihnen irgendetwas glauben zu müssen. Der Sinn eines Beweises liegt nicht darin, dass er überzeugt - das kann eine gute Rede auch -, sondern darin, dass jeder einzelne Schritt darin gar nicht anders hätte ausfallen können.

Das ist eine strengere Forderung, als es klingt. "Es regnet, also ist der Boden nass" ist eine vernünftige Aussage, aber sie stützt sich darauf, was Sie über Regen und Boden wissen. Die formale Logik streicht das und stellt eine engere Frage: Gibt es, allein anhand der Form der Sätze, überhaupt eine Möglichkeit, dass die Prämissen wahr und die Konklusion falsch sind? Gibt es keine, so ist das Argument gültig, und der Beweis ist die Aufzeichnung, warum es keine gibt.

In diesem Leitfaden geht es um eine Art, diese Aufzeichnung herzustellen - die Methode der semantischen Tableaus, auch Wahrheitsbäume genannt. Sie ist die Methode, die diese Seite verwendet, sobald Sie ein Argument in den Rechner eingeben, und wer sie einmal durchlaufen hat, kann ein Argument mit nichts als einem Stift auf Papier prüfen.

2. Gültig - und woran man das erkennt

Schreiben Sie ein Argument mit einem Folgerungsstrich: die Prämissen links, die Konklusion rechts. Die Behauptung p → q, ¬q ⊨ ¬p besagt, dass aus einer Implikation und der Verneinung ihres Konsequens die Verneinung ihres Antezedens folgt. Der Folgerungsstrich ist kein weiterer Junktor. Er ist eine Behauptung über die Formeln zu seinen beiden Seiten, und sie ist entweder richtig oder falsch.

Die Definition der Gültigkeit weist direkt auf ein Prüfverfahren hin: Gehen Sie jede Belegung der Variablen mit wahr und falsch durch und sehen Sie nach, ob eine davon alle Prämissen wahr und die Konklusion falsch macht. Genau das leistet eine Wahrheitstafel, und bei zwei oder drei Variablen ist das völlig in Ordnung. Das Problem ist, dass die Tafel mit 2ⁿ wächst. Zehn Variablen brauchen tausend Zeilen, zwanzig eine Million - und die Tafel sagt nichts darüber, auf welche Zeilen es ankam.

Ein Tableau greift dieselbe Frage von der anderen Seite an. Statt jede Möglichkeit aufzulisten und nach einer schlechten zu suchen, nimmt es an, es gebe eine schlechte, und versucht, sie zu bauen. Bricht der Versuch auf jedem möglichen Weg im Widerspruch zusammen, so gibt es keine solche Belegung und das Argument ist gültig. Gelingt der Versuch, so ist das Gebaute ein Gegenbeispiel, das Sie direkt ablesen können.

3. Die Tableau-Methode

Ein Tableau ist ein Baum signierter Formeln. Jede Zeile ist eine Formel mit einem T oder einem F davor, und das Vorzeichen sagt, was der Ast über diese Formel annimmt - nicht welchen Wahrheitswert sie hat, sondern welchen sie haben müsste, damit das Argument scheitert. Die ganze Methode besteht aus vier Schritten:

1. Schreiben Sie jede Prämisse mit einem T. Sie setzen voraus, dass alle Prämissen des Arguments gelten.
2. Schreiben Sie die Konklusion mit einem F. Sie setzen voraus, dass sie dennoch scheitert - das ist die Annahme, die Sie widerlegen wollen.
3. Nehmen Sie eine Zeile, die noch kein Atom ist, und wenden Sie die Regel für ihren Hauptjunktor und ihr Vorzeichen an; was die Regel liefert, kommt ans Ende jedes Astes, der durch diese Zeile läuft.
4. Schließen Sie einen Ast, sobald er sowohl T A als auch F A für dieselbe Formel A enthält. Hören Sie auf, wenn alle Äste geschlossen sind oder keine Zeile mehr zu zerlegen ist.

Nichts an dieser Schleife verlangt Scharfsinn oder eine Strategiewahl. Zu jeder Zeile gehört genau eine Regel, und die Anwendung in beliebiger Reihenfolge liefert dasselbe Ergebnis - deshalb kann eine Maschine das übernehmen, und deshalb dürfen Sie dem Ergebnis trauen, wenn sie es tut.

4. Die Regeln

Es gibt eine Regel je Junktor und Vorzeichen - zehn insgesamt. Sie zerfallen in zwei Arten, und der Unterschied zwischen ihnen ist der ganze Grund, warum ein Tableau ein Baum ist und keine Liste. Eine α-Regel besagt, dass mehreres zugleich gelten muss, und stapelt ihre Ergebnisse den Ast hinunter. Eine β-Regel besagt, dass eines von zweien gelten muss, spaltet den Ast also in zwei und lässt jeden Fall seinen eigenen Weg gehen.

Jede Regel ist nichts anderes als die Wahrheitsbedingung ihres Junktors, rückwärts gelesen. Eine Konjunktion ist nur wahr, wenn beide Seiten wahr sind, also stapelt T (A ∧ B) sowohl T A als auch T B. Eine Konjunktion ist falsch, wenn mindestens eine Seite falsch ist, aber die Formel sagt nicht welche, also muss F (A ∧ B) beides versuchen: Sie verzweigt. Dieselbe Asymmetrie läuft bei der Disjunktion andersherum, und eine falsche Implikation heißt, dass das Antezedens galt und das Konsequens scheiterte - der eine Fall, in dem eine Implikation bricht.

Beachten Sie, was die Regeln nie tun: Sie erfinden nie eine Formel. Alles, was eine Regel liefert, ist ein Teilstück der Zeile, aus der sie kam. Diese Eigenschaft - die Teilformeleigenschaft - macht das Verfahren endlich, und darauf kommen wir unten zurück.

5. Einen Ast schließen

Ein Ast ist ein einzelner Gedankengang: Lesen Sie von der Wurzel bis zu einem Blatt, und Sie haben eine vollständige Menge von Annahmen. Ein Ast schließt sich, wenn diese Annahmen einander unmittelbar widersprechen, wenn er also sowohl T A als auch F A für ein und dieselbe Formel trägt. Wie kompliziert A ist oder wie weit die beiden Zeilen auseinanderliegen, spielt keine Rolle - verlangt ein Ast, dass eine Formel zugleich wahr und falsch ist, erfüllt ihn nichts.

Markieren Sie einen geschlossenen Ast mit ×, nennen Sie die beiden Zeilen, die ihn geschlossen haben, und arbeiten Sie nicht weiter daran. Aus einer Annahme, die von vornherein unmöglich war, lässt sich nichts mehr lernen.

Wenn sich jeder Ast schließt, ist das Tableau geschlossen, und das ist der Beweis. Er zeigt, dass die Ausgangsvoraussetzung - alle Prämissen wahr, Konklusion falsch - auf jedem möglichen Weg in einen Widerspruch führt. Da kein Weg übrig blieb, gibt es keine solche Belegung, und das Argument ist gültig. Das ist ein Widerspruchsbeweis, so ausgelegt, dass keiner der Fälle übersehen werden kann.

6. Ein Beweis, Zeile für Zeile

Nehmen wir den Modus tollens: p → q, ¬q ⊨ ¬p. Die Zeilen 1 und 2 sind die als wahr angenommenen Prämissen. Zeile 3 ist die als falsch angenommene Konklusion - und da die Konklusion ¬p lautet, heißt sie falsch anzunehmen, p wahr anzunehmen, was Zeile 5 festhält. Zeile 4 stammt aus der Negationsregel, angewandt auf Zeile 2: Ist ¬q wahr, so ist q falsch. Die Implikation in Zeile 1 ist die einzige verbliebene Zeile mit einem Junktor, und sie ist eine β-Regel, also gabelt sich der Baum:

Der linke Ast nimmt an, die Implikation habe gegolten, weil ihr Antezedens scheiterte - aber Zeile 5 hat p bereits wahr, also widerspricht sich der Ast und schließt. Der rechte Ast nimmt an, sie habe gegolten, weil ihr Konsequens wahr war - aber Zeile 4 hat q bereits falsch, also schließt auch er.

Beide Äste sind geschlossen, es gibt also keine Möglichkeit, p → q und ¬q wahr zu haben und ¬p falsch. Das Argument ist gültig, und der Baum ist der Grund. Beachten Sie, dass der Beweis weder Regen noch Boden erwähnt, noch wofür p und q stehen. Er brauchte es nicht.

7. Wenn ein Ast offen bleibt

Nicht jedes Argument ist gültig, und hier zahlt sich die Methode aus. Wenn Sie einen Ast so weit bearbeiten, dass nichts darauf weiter zerlegt werden kann - nur noch Atome und negierte Atome übrig sind -, und er sich trotzdem nicht geschlossen hat, dann ist dieser Ast gesättigt und offen. Er hat sich nicht deshalb nicht geschlossen, weil Sie zu früh aufgehört haben. Es ist nichts mehr zu versuchen.

Ein offener Ast ist mehr als das Urteil "ungültig". Lesen Sie die Vorzeichen seiner Atome ab, und Sie haben eine Belegung: Jedes mit T markierte Atom ist wahr, jedes mit F markierte falsch. Diese Belegung macht alle Prämissen wahr und die Konklusion falsch - genau das, was ein Gegenbeispiel ist. Logiker nennen es ein Gegenmodell, und es ist eine greifbare Antwort auf die Frage "warum nicht?" statt einer Verweigerung.

Die Bejahung des Konsequens, p → q, q ⊨ p, ist der Standardfall. Ihr Tableau lässt einen Ast offen mit p falsch und q wahr - eine Lage, in der die Implikation gilt und ihr Konsequens gilt, das Antezedens aber nicht. Diese eine Belegung widerlegt das Argument für sich allein.

8. Warum es immer endet

Jede Regel ersetzt eine Formel durch deren eigene Teilformeln, und jede Teilformel ist echt kürzer als die Formel, aus der sie stammt. Also kann kein Ast ewig wachsen: Jeder Schritt geht eine endliche Leiter von Bestandteilen des ursprünglichen Arguments hinab, und die Leiter hat ein unteres Ende. Irgendwann ist jede Zeile eines Astes ein Atom oder die Negation eines Atoms, und es bleibt nichts mehr zu tun.

Das ist eine echte Garantie, keine Hoffnung. Es bedeutet, dass die Methode ein Entscheidungsverfahren für die Aussagenlogik ist: Wenden Sie sie auf ein beliebiges Argument an, und sie hält an - mit einem geschlossenen Baum oder einem offenen Ast, und nie mit einem Achselzucken. Der Beweiser dieser Seite setzt darüber hinaus ein Knotenbudget, aber nur als Schutz davor, dass eine pathologische Formel einen Browser-Tab erschöpft - die Mathematik braucht keine solche Schranke.

9. Andere Beweissysteme

Tableaus sind eines von mehreren Beweissystemen, und zwar das widerlegungsförmige: Sie arbeiten, indem sie das Scheitern ausschließen. Der natürliche Schluss geht umgekehrt vor und baut die Konklusion aus den Prämissen vorwärts auf, mit Regeln wie Modus ponens und dem Konditionalbeweis; er liest sich viel eher so, wie ein Mathematiker in Prosa argumentiert. Ein Beweis im natürlichen Schluss ist meist kürzer; ihn zu finden verlangt meist mehr Einfallsreichtum.

Der Sequenzenkalkül formalisiert den Folgerungsstrich selbst und behandelt Folgerungsbehauptungen als Gegenstände, was ihn zum Mittel der Wahl macht, wenn man Aussagen über Beweise beweisen will. Die Resolution führt alles auf Klauseln und eine einzige Regel zurück, was sich unspektakulär liest und außerordentlich schnell läuft - darauf sind die meisten automatischen Beweiser und SAT-Solver gebaut.

Alle stimmen darin überein, welche aussagenlogischen Argumente gültig sind; sie unterscheiden sich darin, wie ein Beweis aussieht und was sich leicht finden lässt. Tableaus sind am freundlichsten zum Lernen, denn ein gescheiterter Beweis ist keine Sackgasse - er liefert Ihnen das Gegenbeispiel.

10. Üben

Am schnellsten lernt man die Methode, indem man sie ausführt. Geben Sie ein Argument mit ⊨, ⊢ oder |= in den Rechner ein, und das Tableau wird neben der Wahrheitstafel gezeichnet, sodass Sie den Baum gegen die Zeilen prüfen können. Arbeiten Sie danach einige Beweise auf Papier durch, bevor Sie nachsehen.