Herbrand-Universum

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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 des Herbrand-Theorems, benannt nach Jacques Herbrand.

Definition[Bearbeiten]

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[Bearbeiten]

F bezeichne eine prädikatenlogische Formel mit

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

H_F ergibt sich zu

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

Man sieht, dass bereits ein Funktionssymbol in F zu einer unendlichen Menge von Termen führt.

Siehe auch[Bearbeiten]