Herbrand-Universum

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

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.

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 :

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.

F bezeichne eine prädikatenlogische Formel mit

Die jeweiligen Teilmengen sehen wie folgt aus:

( Konstante a wurde eingeführt und in eingefügt )

F bezeichne eine prädikatenlogische Formel mit