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 | Quelltext bearbeiten]

Sei eine (geschlossene) Formel in bereinigter Skolemform. Das Herbrand-Universum zu , bezeichnet mit , ist die kleinste Menge von Termen, die folgende Bedingungen erfüllt:

  1. Ist eine in vorkommende Konstante, dann ist .
  2. Kommt in keine Konstante vor, so wird eine neue Konstante eingeführt und in aufgenommen.
  3. ist induktiv definiert durch . Dabei ist eine Menge von Termen, die sich mittels der in vorkommenden Funktionssymbole und den bereits konstruierten Termen aus bilden lassen. Sei beispielsweise ein solches n-stelliges Funktionssymbol und seien Terme aus , dann ist . Jeder so durch Funktionssymbole aus und Terme aus bildbare Term ist Element von .

Daraus ergibt sich das Herbrand-Universum zu :

Beispiel[Bearbeiten | Quelltext bearbeiten]

F bezeichne eine prädikatenlogische Formel mit

ergibt sich zu

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

Siehe auch[Bearbeiten | Quelltext bearbeiten]