Herbrand-Universum
aus Wikipedia, der freien Enzyklopädie
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 der Herbrand-Theorie, benannt nach Jacques Herbrand.
[Bearbeiten] Definition
Sei F eine (geschlossene) Formel in bereinigter Skolemform. Das Herbrand-Universum zu F, bezeichnet mit HF, ist die kleinste Menge von Termen, die folgende Bedingungen erfüllt:
- Ist k eine in F vorkommende Konstante, dann ist
. - Kommt in F keine Konstante vor, so wird eine neue Konstante a eingeführt und in H0 aufgenommen.
- Hk + 1 ist induktiv definiert durch
. Dabei ist G eine Menge von Termen, die sich mittels der in F vorkommenden Funktionssymbole und den bereits konstruierten Termen aus Hk bilden lassen. Sei beispielsweise g ein solches n-stelliges Funktionssymbol und seien t1,t2,...,tn Terme aus Hk, dann ist 
. Jeder so durch Funktionssymbole aus F und Terme aus Hk bildbare Term ist Element von Hk + 1.
Daraus ergibt sich das Herbrand-Universum zu F:
[Bearbeiten] Beispiel
F bezeichne eine prädikatenlogische Formel mit
HF ergibt sich zu
Man sieht, dass bereits ein Funktionssymbol in F zu einer unendlich großen Menge von Termen führt.
