Herbrand-Interpretation

In der mathematischen Logik ist eine Herbrand-Interpretation einer Sprache der Logik erster Stufe mit Signatur $𝒮$ eine $𝒮$-Interpretation $ℐ=(U,I)$, bei der das Universum $U$ das Herbrand-Universum über $𝒮$, 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 $f\in 𝒮$ durch die Funktion $f^I:U\to U;t\mapsto f(t)$ interpretiert. Die Menge $HB$ der einfachen Aussagen heißt Herbrand-Basis zu $𝒮$. Die Interpretation der Relationssymbole ist nun vollständig spezifiziert durch eine Teilmenge $𝒜\subseteq HB$ der Herbrand-Basis, wobei jedes $n$-stellige Relationssymbol $R\in 𝒮$ durch die Relation $R^I=\{(t_1,\dots ,t_n)\in U^n\mid R(t_1,\dots ,t_n)\in 𝒜\}$ interpretiert wird.

Beispiel

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

$f^I(a)=f(a)$

$f^I(f(a))=f(f(a))$

$f^I(f(f(a)))=f(f(f(a)))$

...