Herbrand-Interpretation

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