Begriff
Herbrand Universe
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
In der Logik reden wir über "Objekte".
$\forall x (Mensch(x) \to Sterblich(x))$.
Was sind diese $x$? Hans? Sokrates? Der Stuhl?
Das Universum kann unendlich groß sein.
Wie kann ein Computer alle Objekte prüfen?
Jacques Herbrand (1930) hatte eine geniale Idee:
Wir ignorieren die echte Welt. Wir bauen eine Welt nur aus Wörtern (Symbolen).
Wenn wir die Konstante a und die Funktion f haben.
Dann ist das Herbrand-Universum: { a, f(a), f(f(a)), ... }.
Wenn eine Formel hier gilt, können wir Aussagen über ihre Gültigkeit machen.
Es reduziert die unendliche Semantik auf pure Syntax.
Merksatz: Die Menge aller Grundterme, die aus den Konstanten und Funktionssymbolen einer logischen Formel gebildet werden können; sie dient als fundamentales Modell in der automatischen Beweisführung.
Es ist das Fundament von Prolog.
In Prolog gibt es keine "echten Objekte" (wie Pointer auf Speicher).
Es gibt nur Terme (vater(hans)).
Prolog rechnet im Herbrand-Universum.
X = vater(hans). Das ist ein syntaktischer Match.
1. Satz von Herbrand
Der wichtigste Satz.
Eine Formel ($\exists x F(x)$) ist genau dann beweisbar, wenn eine endliche Menge von Herbrand-Instanzen ($F(t_1) \lor F(t_2) \dots$) gültig ist.
Das heißt: Man muss nicht unendlich suchen.
Man kann Instanzen generieren (a, f(a), f(f(a))).
Irgendwann muss der Beweis auftauchen (wenn es einen gibt).
Das war der Startschuss für Automated Theorem Proving.
1. Herbrand-Basis & Interpretationen
Das Herbrand-Universum liefert die "Substantive". Die Herbrand-Basis liefert die "Sätze".
Sie besteht aus allen möglichen Kombinationen von Prädikaten mit den Termen des Universums (z. B. Sterblich(a), Sterblich(f(a)), ...).
Eine Herbrand-Interpretation ist dann einfach eine Teilmenge dieser Basis, die wir als "wahr" definieren.
Das Geniale: In der Prädikatenlogik 1. Ordnung reicht es völlig aus, nur diese Herbrand-Interpretationen zu prüfen. Wenn eine Formel in keiner Herbrand-Interpretation wahr ist, dann ist sie in überhaupt keinem mathematischen Modell wahr (Unerfüllbarkeit). Das macht die Suche nach Gegenbeispielen für Computer erst möglich.
2. Skolem-Herbrand-Gödelscher Satz
Oft als SHG-Satz bezeichnet, schlägt er die Brücke zur Aussagenlogik. Man kann eine Formel der Prädikatenlogik (mit Quantoren $\forall, \exists$) schrittweise "entrollen", indem man die Variablen durch Terme aus dem Herbrand-Universum ersetzt. Dadurch entsteht eine (potenziell unendliche) Liste von Aussagen ohne Quantoren. Moderne Automated Theorem Prover nutzen diesen Satz, indem sie sukzessive größere Mengen dieser "Instanzen" an einen SAT-Solver schicken. Sobald der SAT-Solver "Unerfüllbar" meldet, ist das ursprüngliche Problem bewiesen. Der Computer hat das unendliche Logikproblem also mundgerecht in endliche Häppchen zerteilt.
3. Löwenheim-Skolem Interaction
Aus Herbrands Theorie folgt auch eine seltsame Konsequenz: Wenn eine Theorie ein unendliches Modell hat, dann hat sie auch ein Modell in der Größe des Herbrand-Universums (abzählbar unendlich). Das bedeutet, dass Logik 1. Ordnung den Unterschied zwischen verschiedenen Unendlichkeiten (z. B. reelle Zahlen vs. natürliche Zahlen) nicht "spüren" kann. Dies führt zum Skolem-Paradoxon und zeigt die Grenzen auf, wie präzise wir mathematische Strukturen überhaupt mit Computern und Logik beschreiben können.
Quick-Check
Unendlich?
Ja, das Universum ist meist abzählbar unendlich (wie Strings). Aber jeder einzelne Term ist endlich.Tragiker?
Jacques Herbrand starb mit 23 Jahren beim Bergsteigen. Ein Genie wie Galois oder Abel. Wer weiß, was er noch entdeckt hätte.Zusammenhang zu Resolution?
Resolution arbeitet auf dem Herbrand-Universum (durch Unifikation). Es ist die praktische Umsetzung von Herbrands Theorie.