Seit einem Monat arbeite ich mich durch ein japanisches Einführungslehrbuch der Logik, ein Kapitel pro Tag, und übersetze dabei jeden Beweis in kleine Haskell-Schnipsel. Ich hätte nicht erwartet, dass ein Lehrbuch aus dem Jahr 2000 über Aussagen- und Prädikatenlogik verändert, wie ich darüber denke, warum manche meiner Werkzeuge hängenbleiben und andere nicht. Aber irgendwo in Kapitel 7 ist genau das passiert.

Hier die Grundform des Arguments, ohne das Japanische und ohne den Code.

Das kostenlose Mittagessen der Aussagenlogik

Die Aussagenlogik — die Logik von “und”, “oder”, “nicht”, “wenn-dann”, angewendet auf atomare Aussagen ohne innere Struktur — bringt etwas mit, das zunächst wie eine Superkraft wirkt. Jede Frage, die sich in ihrer Sprache stellen lässt (“ist diese Formel eine Tautologie”, “sind diese beiden Formeln äquivalent”, “folgt dieses Argument gültig aus seinen Prämissen”) lässt sich mit brachialer Gewalt entscheiden: alle möglichen Belegungen der atomaren Aussagen mit wahr/falsch aufzählen, jede Zeile prüfen, fertig. Bei n atomaren Aussagen gibt es 2^n Zeilen. Die Tabelle ist endlich, das Verfahren terminiert immer, und es liefert immer ein eindeutiges Ja oder Nein. Das ist Entscheidbarkeit, und die Aussagenlogik hat sie umsonst.

Es lohnt sich, kurz zu verweilen, warum das überhaupt möglich ist. Wahrheitstafeln liefern eine erschöpfende Suche über den ganzen Möglichkeitsraum, und das funktioniert nur, weil dieser Raum endlich ist. In dem Moment, in dem sich jeder Fall aufzählen lässt, wird Testen zum Beweis — der scheinbare Widerspruch zwischen Edsger Dijkstras berühmtem Satz, Testen könne die Anwesenheit von Fehlern zeigen, aber niemals deren Abwesenheit, und den selbstbewussten 2^n-Zeilen-Tabellen dieses Lehrbuchs löst sich auf, sobald man merkt, dass beide dieselbe Tatsache von entgegengesetzten Seiten beschreiben. Dijkstras Warnung betrifft unendliche Eingaberäume, in denen eine Testsuite notwendigerweise eine Stichprobe bleibt. Eine Wahrheitstafel ist keine Stichprobe. Sie ist eine Vollerhebung.

Der Haken, und er ist ernst, ist, dass diese Vollständigkeit aus mangelndem Ehrgeiz kommt. Die Aussagenlogik kann nicht über Individuen sprechen, über deren Eigenschaften oder über Beziehungen zwischen ihnen. Sie kann nicht ausdrücken “jeder liebt jemanden” oder “es gibt einen Pfad von A nach B”. Ihr gesamter semantischer Gehalt wird von einer Funktion von der endlichen Menge der atomaren Wahrheitswerte auf einen Wahrheitswert erfasst — das heißt, so viele Formeln man auch aufschreiben kann, es gibt nur 2^(2^n) wirklich verschiedene Bedeutungen, die n Atome ausdrücken können. Die Syntax ist unendlich, die Semantik ist endlich. Genau diese Lücke ist der Spielraum, der erschöpfendes Prüfen erst möglich macht.

Wo der Boden wegbricht

Die Prädikatenlogik fügt Quantoren (“für alle”, “es gibt”) und Relationen zwischen Individuen hinzu, und hier endet das kostenlose Mittagessen. In dem Moment, in dem die Sprache Dinge sagen kann wie “für jedes x gibt es ein y, sodass R(x, y)” — das Schema hinter Behauptungen über Pfade in einem Graphen, Erreichbarkeit, Ketten von Beziehungen — ist der endliche semantische Gehalt der Aussagenlogik verschwunden. Die Beziehungen eines Individuums zu anderen Individuen lassen sich nicht auf eine endliche Tabelle zusammenfalten, wie es bei einer Wahrheitswertbelegung möglich ist.

Bemerkenswert ist, wie sich das operational zeigt, nicht nur als Satzaussage. Das Lehrbuch geht ein Beweissuchverfahren (eine Tableau-Methode) zur Gültigkeitsprüfung durch, und darin steckt eine strukturelle Asymmetrie: Die Regel für den Existenzquantor feuert einmal pro Formel und ist dann fertig — sie führt ein neues Individuum ein und ist damit erledigt. Die Regel für den Allquantor kann beliebig oft erneut angewendet werden, auf jedes Individuum, das im Beweis an irgendeinem Punkt auftaucht, einschließlich solcher, die durch spätere Schritte erzeugt wurden. In der Aussagenlogik ist diese Asymmetrie unsichtbar, weil die “Individuen” nur Wahrheitswerte sind und es davon nur 2^n gibt; die Suche kommt immer zu einem Ende. In der vollen Prädikatenlogik kann eine Formel wie “für alle x existiert ein y, sodass R(x,y)” eine Kette auslösen — ein Individuum einführen, um die Existenzforderung zu erfüllen, die Allregel darauf anwenden, eine neue Existenzforderung erhalten, ein weiteres Individuum einführen, die Allregel erneut anwenden — die kein garantiertes Ende hat. Das ist strukturell identisch mit einer Prolog-Anfrage, die versucht, eine rekursive Klausel zu erfüllen, und nie zurückkehrt, und das ist kein Zufall: automatische Beweiser sind genau auf dieser Art von Suche aufgebaut.

Das ist kein Mangel dieser bestimmten Beweismethode. Es ist ein Symptom von etwas, das Alonzo Church und Alan Turing 1936 unabhängig voneinander bewiesen, mit völlig verschiedenen formalen Mitteln (Church mit dem Lambda-Kalkül, Turing mit dem, was wir heute Turingmaschine nennen): Die Frage “ist diese Formel der Prädikatenlogik gültig?” lässt sich durch keinen Algorithmus beantworten, der bei jeder Eingabe garantiert terminiert. Das war Hilberts Entscheidungsproblem, und die Antwort, auf zwei verschiedenen Wegen erreicht, lautete beide Male Nein.1 Das Kapitel, das dieses Ergebnis behandelt, trägt den bewusst beruhigenden Titel “Gebt den Logikern nicht die Schuld” — der Punkt ist, dass dies kein Versagen an Cleverness ist. Ein klügeres Suchverfahren kann das nicht beheben, weil die Einschränkung eine bewiesene mathematische Tatsache darüber ist, was die Klasse der Algorithmen leisten kann, keine Lücke, die einfach noch nicht geschlossen wurde.

Die Asymmetrie, die übrig bleibt

Statt Entscheidbarkeit bekommt man Semi-Entscheidbarkeit: Ist eine Formel gültig, garantiert irgendein Suchverfahren, dies irgendwann zu bestätigen und zu terminieren. Ist eine Formel ungültig, garantiert kein Verfahren, einem das mitzuteilen — es könnte ewig laufen, und eine Suche, die schon sehr lange ohne Beweis läuft, gibt einem keine Möglichkeit, “das ist ungültig” von “der Beweis ist noch da draußen” zu unterscheiden. Gödels Vollständigkeitssatz garantiert die “Ja”-Seite: Die Menge der gültigen Formeln ist rekursiv aufzählbar, sodass systematisches Aufzählen und Prüfen von Beweiskandidaten irgendwann einen zutage fördert, falls einer existiert.2 Nichts Vergleichbares rettet die “Nein”-Seite, und das ist kein Versehen — es ist beweisbar äquivalent zum Halteproblem. Man kann “hält dieses Programm an” als “ist diese Formel gültig” kodieren, auf eine Weise, die zeigt, dass jeder allgemeine Gültigkeitsentscheider auch das Halteproblem entscheiden würde, was bereits als unmöglich bekannt ist.

Das empfand ich eher als befriedigend denn als niederschmetternd, weil es etwas benennt, dem ich immer wieder begegne, ohne einen Namen dafür zu haben. Typinferenz in einer Sprache mit hinreichend ausdrucksstarkem Typsystem (Rangpolymorphie, abhängige Typen) kann hängenbleiben. SMT-Solver können hängenbleiben. Paketversions-Resolver, die sich auf Erfüllbarkeit zurückführen lassen, können hängenbleiben. In jedem Fall steckt darunter eine Designentscheidung: Bleibt das Werkzeug innerhalb eines Fragments der Logik, das klein genug ist, um Terminierung zu garantieren, und gibt dafür Ausdruckskraft auf — oder nimmt es die Ausdruckskraft und akzeptiert, dass die Antwort in der Praxis manchmal ein Timeout ist? Typsystem-Designer scheinen häufiger zur ersten Wahl zu tendieren als die Welt der automatisierten Beweisführung und der Logikprogrammierung, und ich habe noch keine überzeugende Erklärung dafür, warum sich die Kulturen so aufspalten, statt dass das Feld konsistent wäre. Vielleicht ist es einfach so, dass ein Typprüfer, der gelegentlich das Kompilieren verweigert, erträglicher ist als einer, der gelegentlich den Build zum Hängen bringt.

Es gibt noch etwas, worauf das Buch durchweg sorgfältig achtet: Die Behauptung, dass Turingmaschinen und Lambda-Kalkül beide “die” korrekte Formalisierung des informellen, vortheoretischen Begriffs der “Berechnung” erfassen — die Church-Turing-These —, wird aus einem echten Grund als These und nicht als Satz bezeichnet. Dass zwei unabhängig voneinander erfundene formale Systeme sich als äquivalent zueinander erweisen, ist ein Satz, beweisbar innerhalb der Mathematik. Dass dieser gemeinsame Begriff die richtige Formalisierung des unscharfen menschlichen Konzepts “was berechenbar ist” darstellt, ist nichts, was die Mathematik verifizieren kann, weil das unscharfe menschliche Konzept nie selbst ein mathematisches Objekt war. Das ist eine Aussage über die Welt, gestützt durch die Tatsache, dass jeder nachfolgende Versuch, Berechnung zu formalisieren — rekursive Funktionen, Registermaschinen, zelluläre Automaten — auf derselben Äquivalenzklasse gelandet ist, bleibt aber, ehrlich gesagt, eine induktive Behauptung statt ein Beweis. Mir gefällt, dass das Buch darauf besteht, diese Grenze zu markieren, statt sie zu verwischen, denn die Grenze zwischen dem, was bewiesen ist, und dem, was bloß noch nie widerlegt wurde, ist genau die Art von Unterscheidung, die leicht verschwimmt, sobald eine Behauptung oft genug bestätigt wurde.

Eine offene Frage

Was mich noch beschäftigt, ist praktischer, nicht technischer Natur. Wenn man weiß, dass ein Problem hinter so einer Mauer liegt — wirklich unentscheidbar, nicht nur schwer —, scheint es genau zwei mögliche Züge zu geben: die Sprache verkleinern, bis man wieder in einem entscheidbaren Fragment landet, oder die Ausdruckskraft behalten und das Risiko der Nichtterminierung mit Heuristiken, Tiefenbegrenzungen und Timeouts im Betrieb managen. Beides sind legitime Ingenieursentscheidungen, und verschiedene Communities scheinen konventionsgemäß entgegengesetzte Wetten abgeschlossen zu haben, ohne dass ich ein Argument dafür benennen könnte. Ich glaube nicht, dass es hier eine einzige richtige Antwort gibt — aber mich würde interessieren, ob schon jemand tatsächlich formalisiert hat, warum sich diese beiden Kulturen so aufgespalten haben, statt dass es einfach so ist, wie die Felder zufällig gewachsen sind.

  1. Entscheidungsproblem. Wikipedia. Accessed 2026-08-11. ↩

  2. Gödel’s completeness theorem. Wikipedia. Accessed 2026-08-11. ↩