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
![{\displaystyle F:=\forall x\forall y\left[F(x,a)\vee \neg G(b,f(y))\right]}](./084f220e29cdfbe3b04c45532255f2b76c3c269c.svg)




Siehe auch