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

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

Daraus ergibt sich das Herbrand-Universum zu ${\displaystyle F}$:

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

Beispiel

F bezeichne eine prädikatenlogische Formel mit

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

${\displaystyle H_{F}}$ ergibt sich zu

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

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

Beispiel 2

F bezeichne eine prädikatenlogische Formel mit

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

Die jeweiligen Teilmengen sehen wie folgt aus:

${\displaystyle H_{0}=\{a\}}$ ( Konstante a wurde eingeführt und in ${\displaystyle H_{0}}$ eingefügt )

${\displaystyle H_{1}=\{a,f(a),g(a)\}}$

${\displaystyle H_{2}=\{a,f(a),g(a),f(f(a)),f(g(a)),g(f(a)),g(g(a))\}}$

${\displaystyle H_{3}=H_{2}\cup \dots }$

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

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]}$

${\displaystyle H_{0}=\{a,b\}}$

${\displaystyle H_{1}=\{a,b,f(a),f(b)\}}$

${\displaystyle H_{2}=\{a,b,f(a),f(b),f(f(a)),f(f(b)),\dots \}}$

${\displaystyle \dots }$

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

Siehe auch

• Satz von Herbrand
• Herbrand-Interpretation