Herbrand-Universum
# Herbrand-Universum

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 $F$ eine (geschlossene) Formel in bereinigter Skolemform. Das Herbrand-Universum zu $F$, bezeichnet mit $H_{F}$, ist die kleinste Menge von Termen, die folgende Bedingungen erfüllt:

* Ist $c$ eine in $F$ vorkommende Konstante, dann ist $c\in H_{0}$.
* Kommt in $F$ keine Konstante vor, so wird eine neue Konstante $a$ eingeführt und in $H_{0}$ aufgenommen.
* $H_{k+1}$ ist induktiv definiert durch $H_{k}\cup G$. Dabei ist $G$ eine Menge von Termen, die sich mittels der in $F$ vorkommenden Funktionssymbole und den bereits konstruierten Termen aus $H_{k}$ bilden lassen. Sei beispielsweise $g$ ein solches n-stelliges Funktionssymbol und seien $t_{1},t_{2},...,t_{n}$ Terme aus $H_{k}$, dann ist $g(t_{1},t_{2},...,t_{n})\in H_{k+1}$. Jeder so durch Funktionssymbole aus $F$ und Terme aus $H_{k}$ bildbare Term ist Element von $H_{k+1}$.

Daraus ergibt sich das Herbrand-Universum zu $F$:

$H_{F}=\bigcup _{k\geq 0}H_{k}$

### Beispiel

F bezeichne eine prädikatenlogische Formel mit

    $F:=\forall x\forall y\left(P\left(x,a\right)\vee Q\left(x,f\left(y\right)\right)\right)$

$H_{F}$ ergibt sich zu

    $H_{F}=\left\{a,f\left(a\right),f\left(f\left(a\right)\right),\ldots \right\}$

Man sieht, dass bereits ein Funktionssymbol in $F$ zu einer unendlichen Menge von Termen führt.

### Beispiel 2

F bezeichne eine prädikatenlogische Formel mit

    $F:=\forall x\forall y\left(f(x)\vee g(y)\right)$

Die jeweiligen Teilmengen sehen wie folgt aus:

    $H_{0}=\{a\}$ ( Konstante a wurde eingeführt und in $H_{0}$ eingefügt )
    $H_{1}=\{a,f(a),g(a)\}$
    $H_{2}=\{a,f(a),g(a),f(f(a)),f(g(a)),g(f(a)),g(g(a))\}$
    $H_{3}=H_{2}\cup \dots$

$H_{F}=\lim _{n\to \infty }H_{n}$

### Beispiel 3

F bezeichne eine prädikatenlogische Formel mit

    $F:=\forall x\forall y\left[F(x,a)\vee \neg G(b,f(y))\right]$
    $H_{0}=\{a,b\}$
    $H_{1}=\{a,b,f(a),f(b)\}$
    $H_{2}=\{a,b,f(a),f(b),f(f(a)),f(f(b)),\dots \}$
    $\dots$

$H_{F}=\lim _{n\to \infty }H_{n}=H_{0}\cup H_{1}\cup H_{2}\cup\dots$

