Das Herbrand-Universum ist eine Menge in der Prädikatenlogik, die als Grundmenge zur Definition der Herbrand-Struktur herangezogen wird. Beide Begriffe sind Teil des Herbrand-Theorems, benannt nach Jacques Herbrand.
Definition Sei eine (geschlossene) Formel in bereinigter Skolemform. Das Herbrand-Universum zu , bezeichnet mit , ist die kleinste Menge von Termen, die folgende Bedingungen erfüllt:
Ist eine in vorkommende Konstante, dann ist . Kommt in keine Konstante vor, so wird eine neue Konstante eingeführt und in aufgenommen. ist induktiv definiert durch . Dabei ist eine Menge von Termen, die sich mittels der in vorkommenden Funktionssymbole und den bereits konstruierten Termen aus bilden lassen. Sei beispielsweise ein solches n-stelliges Funktionssymbol und seien Terme aus , dann ist . Jeder so durch Funktionssymbole aus und Terme aus bildbare Term ist Element von .
Daraus ergibt sich das Herbrand-Universum zu :
Beispiel F bezeichne eine prädikatenlogische Formel mit
ergibt sich zu
Man sieht, dass bereits ein Funktionssymbol in zu einer unendlichen Menge von Termen führt.
Beispiel 2 F bezeichne eine prädikatenlogische Formel mit
Die jeweiligen Teilmengen sehen wie folgt aus: ( Konstante a wurde eingeführt und in eingefügt )
Beispiel 3 F bezeichne eine prädikatenlogische Formel mit
Siehe auch Satz von Herbrand Herbrand-Interpretation
Kategorie:Mathematische Logik