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:

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:=\mathrm{\forall }x\mathrm{\forall }y(P(x,a)\vee Q(x,f\left(y\right)))$

$H_F$ ergibt sich zu

$H_F=\{a,f\left(a\right),f\left(f\left(a\right)\right),\dots \}$

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:=\mathrm{\forall }x\mathrm{\forall }y(f(x)\vee g(y))$

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=\underset{n\to \mathrm{\infty }}{\lim }{H}_n$

Beispiel 3

F bezeichne eine prädikatenlogische Formel mit

$F:=\mathrm{\forall }x\mathrm{\forall }y[F(x,a)\vee \mathrm{\neg }G(b,f(y))]$

$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=\underset{n\to \mathrm{\infty }}{\lim }{H}_n=H_0\cup H_1\cup H_2\cup \dots$

Siehe auch

• Satz von Herbrand
• Herbrand-Interpretation