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₀ 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₁,t₂,...,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