Herbrand-Universum

Mit Herbrand-Universum bezeichnet man 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:

1. Ist $c$ eine in $F$ vorkommende Konstante, dann ist $c \in H_0$.
2. Kommt in $F$ keine Konstante vor, so wird eine neue Konstante $a$ eingeführt und in $H_0$ aufgenommen.
3. $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\ge 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.

Siehe auch

• Satz von Herbrand