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 H_F, ist die kleinste Menge von Termen, die folgende Bedingungen erfüllt:

1. Ist k eine in F vorkommende Konstante, dann ist .
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 . 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 . 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:

[Bearbeiten] Beispiel

F bezeichne eine prädikatenlogische Formel mit

H_F ergibt sich zu

Man sieht, dass bereits ein Funktionssymbol in F zu einer unendlich großen Menge von Termen führt.

[Bearbeiten] Siehe auch

• Satz von Herbrand