Herbrand-Interpretation

In der mathematischen Logik ist eine Herbrand-Interpretation einer Sprache der Logik erster Stufe mit Signatur <math> \mathcal{S} </math> eine <math>\mathcal{S}</math>-Interpretation <math> \mathcal{I} = (U,I) </math>, bei der das Universum <math>U</math> das Herbrand-Universum über <math>\mathcal{S}</math>, d. h. die Menge aller Terme ohne Variablen, ist, und jeder Term „durch sich selbst“ interpretiert wird. Somit lässt sich eine Herbrand-Interpretation vollständig durch die Angabe der Interpretation der Relationssymbole beschreiben.

Formal wird jedes Funktionssymbol <math> f \in \mathcal{S} </math> durch die Funktion <math>f^I \colon U \to U; \ t \mapsto f(t) </math> interpretiert. Die Menge <math> HB </math> der einfachen Aussagen heißt Herbrand-Basis zu <math> \mathcal S </math>. Die Interpretation der Relationssymbole ist nun vollständig spezifiziert durch eine Teilmenge <math> \mathcal A \subseteq HB </math> der Herbrand-Basis, wobei jedes <math>n</math>-stellige Relationssymbol <math> R \in \mathcal{S} </math> durch die Relation <math> R^I = \{(t_1,\dotsc,t_n) \in U^n \mid R(t_1,\dotsc,t_n) \in \mathcal A\} </math> interpretiert wird.

Beispiel

Enthalte die Signatur <math> S </math> nur das Konstantensymbol <math> a </math> und das Funktionssymbol <math> f </math>. Das zugehörige Herbrand-Universum ist <math>D\left(\mathcal{S}\right) = \{ a, f(a), f(f(a)), ... \}</math>. Dann lautet die Zuordnung zwischen Funktionssymbolen und Elementen aus dem Universum:

...