Die Menge aller ground (variablenfreien) Terme, die aus den Konstanten- und Funktionssymbolen einer prädikatenlogischen Sprache gebildet werden können.

Prinzip

Man bildet die kleinste Termalgebra, die unter den Konstanten und Funktionssymbolen der Signatur abgeschlossen ist; Variablen sind ausgeschlossen, sodass wiederholte Anwendung von Funktionen auf bereits gebildete ground-Terme die Menge erzeugt.

Demonstration

Für eine Signatur mit Konstante a und einer einstelligen Funktion f ist das Herbrand-Universum {a, f(a), f(f(a)), ...}, häufig unendlich, durch wiederholte Anwendung von f auf a erzeugt.

Fehlanwendung

Das Herbrand-Universum fälschlich als semantische Domäne mit interpretierten Objekten zu behandeln oder es als endlich anzunehmen, obwohl die Signatur Funktionssymbole hat, die unendlich viele Terme erzeugen.

Konsequenz

Stellt eine rein syntaktische Domäne für die Konstruktion grounder Instanzen von Formeln bereit und bildet die Grundlage für Herbrand-Interpretationen und -Modelle in der automatischen Theorembeweisung und Logikprogrammierung.

Umkehrung

Statt der ground-Term-Abschließung betrachtet man die Menge nicht-groundlicher Terme (mit Variablen) oder eine interpretierte Domäne mit semantischen Elementen — der Fokus verlagert sich von syntaktischer Termbildung zu semantischer Interpretation.

Abgrenzung

Enthält nur ground-Terme, die aus Konstanten und Funktionen der Sprache gebildet werden; schließt Variablen, Prädikatsymbole, Metaterme und externe Symbole aus und legt an sich keine Wahrheitswerte fest.

Semantische Spannung

Spannung zwischen dem Herbrand-Universum als rein syntaktischer Termalgebra und dem modelltheoretischen Begriff einer Domäne: Beides wird als 'Domäne' bezeichnet, bedeutet aber Verschiedenes.

Synthese

Das Herbrand-Universum ist die syntaktische Welt der ground-Terme, erzeugt aus den Konstanten und Funktionen einer Signatur; es dient dazu, Formeln zu grounden, die Herbrand-Basis zu bilden und syntaktische Beweistechniken mit modelltheoretischem Denken zu verknüpfen.