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 <math>F</math> eine (geschlossene) Formel in bereinigter Skolemform. Das Herbrand-Universum zu <math>F</math>, bezeichnet mit <math>H_F</math>, ist die kleinste Menge von Termen, die folgende Bedingungen erfüllt:
- Ist <math>c</math> eine in <math>F</math> vorkommende Konstante, dann ist <math>c \in H_0</math>.
- Kommt in <math>F</math> keine Konstante vor, so wird eine neue Konstante <math>a</math> eingeführt und in <math>H_0</math> aufgenommen.
- <math>H_{k+1}</math> ist induktiv definiert durch <math>H_k \cup G</math>. Dabei ist <math>G</math> eine Menge von Termen, die sich mittels der in <math>F</math> vorkommenden Funktionssymbole und den bereits konstruierten Termen aus <math>H_k</math> bilden lassen. Sei beispielsweise <math>g</math> ein solches n-stelliges Funktionssymbol und seien <math>t_1, t_2, ..., t_n</math> Terme aus <math>H_k</math>, dann ist <math>g(t_1, t_2, ..., t_n) \in H_{k+1}</math>. Jeder so durch Funktionssymbole aus <math>F</math> und Terme aus <math>H_k</math> bildbare Term ist Element von <math>H_{k+1}</math>.
Daraus ergibt sich das Herbrand-Universum zu <math>F</math>:
<math>H_F = \bigcup_{k\ge 0} H_{k}</math>
Beispiel
F bezeichne eine prädikatenlogische Formel mit
- <math>F:=\forall x \forall y \left( P\left(x,a\right) \vee Q\left(x,f\left(y\right)\right)\right)</math>
<math>H_F</math> ergibt sich zu
- <math>H_F=\left\{a,f\left(a\right),f\left(f\left(a\right)\right), \ldots\right\}</math>
Man sieht, dass bereits ein Funktionssymbol in <math>F</math> zu einer unendlichen Menge von Termen führt.
Beispiel 2
F bezeichne eine prädikatenlogische Formel mit
- <math>F:=\forall x \forall y \left( f(x) \vee g(y)\right)</math>
Die jeweiligen Teilmengen sehen wie folgt aus:
- <math>H_0 = \{a\} </math> ( Konstante a wurde eingeführt und in <math>H_0</math> eingefügt )
- <math>H_1 = \{a, f(a), g(a) \}</math>
- <math>H_2 = \{a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), g(g(a)) \}</math>
- <math>H_3 = H_2 \cup \dots </math>
<math>H_F = \lim_{n \to \infty} H_n </math>
Beispiel 3
F bezeichne eine prädikatenlogische Formel mit
- <math>F:=\forall x \forall y \left[ F(x,a) \vee \neg G(b,f(y)) \right]</math>
- <math>H_0 = \{a, b\} </math>
- <math>H_1 = \{a, b, f(a), f(b) \}</math>
- <math>H_2 = \{a, b, f(a), f(b), f(f(a)), f(f(b)), \dots \}</math>
- <math>\dots </math>
<math>H_F = \lim_{n \to \infty} H_n = H_0 \cup H_1 \cup H_2 \cup {} \dots </math>