Terminterpretation

Die Terminterpretation ist ein Begriff aus der mathematischen Logik, es handelt sich um eine spezielle Interpretation in der Prädikatenlogik erster Stufe.

Ist eine Menge $\Phi$ von Ausdrücken einer Sprache $L_{I}^{S}$ gegeben, so soll eine von $\Phi$ abhängige Interpretation der Sprache konstruiert werden. Diese verwendet im Wesentlichen die Terme der Sprache. Eine Interpretation ist durch ihr Universum (nicht-leere Menge), durch eine Interpretation der Symbole in $S$ und eine Variablenbelegung gegeben. Wir beginnen mit der Festlegung des Universums der Interpretation. Durch

$t_{1}\sim t_{2}\quad \Leftrightarrow \quad \Phi \vdash t_{1}\equiv t_{2}$

wird eine Äquivalenzrelation auf der Menge $T$ aller Terme der Sprache definiert. Die Menge $T/\sim$ der Äquivalenzklassen wird mit $T^{\Phi }\,$ bezeichnet, die Äquivalenzklasse eines Terms mit $[t]_{\Phi }\,$. Wir verwenden $T^{\Phi }\,$ als Universum einer Interpretation ${\mathcal {T}}^{\Phi }$.

Als Nächstes sind die Interpretationen der Konstanten-, Funktions- und Relationssymbole anzugeben. Für ein Konstantensymbol $c$ setze

$c^{{\mathcal {T}}^{\Phi }}\quad :=\quad [c]_{\Phi }\in T^{\Phi }$.

Für ein n-stelliges Funktionssymbol $f$ definiere

$f^{{\mathcal {T}}^{\Phi }}:(T^{\Phi })^{n}\rightarrow T^{\Phi },\quad f^{{\mathcal {T}}^{\Phi }}([t_{1}]_{\Phi },\ldots ,[t_{n}]_{\Phi }):=[ft_{1}\ldots t_{n}]_{\Phi }$

und für ein n-stelliges Relationssymbol $R$

$R^{{\mathcal {T}}^{\Phi }}([t_{1}]_{\Phi },\ldots ,[t_{n}]_{\Phi })\quad :\Leftrightarrow \quad \Phi \vdash Rt_{1}\ldots t_{n}$.

Man kann zeigen, dass diese Festlegungen wohldefiniert sind. Schließlich ist noch eine Variablenbelegung $\beta ^{\Phi }$ anzugeben; man setzt einfach

$\beta ^{\Phi }(v_{i})\,:=\,[v_{i}]_{\Phi }$, wobei $v_{0},v_{1},v_{2},\ldots$ die Variablen seien.

Insgesamt ist dadurch die sogenannte Terminterpretation ${\mathcal {T}}^{\Phi }=(T^{\Phi },\beta ^{\Phi })$ definiert.

Obigen Definitionen sieht man sofort an, dass durch

$T_{k}^{\Phi }:=\{[t]_{\Phi };\,t\in T,\mathrm {var} (t)\subset \{v_{0},\ldots v_{k-1}\}\}$

Unterstrukturen definiert sind, wobei $\mathrm {var} (t)$ für die Menge der im Term $t$ vorkommenden Variablen steht und die Symbolmenge im Falle $k=0$ wenigstens ein Konstantensymbol $c$ enthalten muss, damit $T_{k}^{\Phi }$ nicht leer ist. Man erhält so weitere Interpretationen ${\mathcal {T}}_{k}^{\Phi }=(T_{k}^{\Phi },\beta _{k}^{\Phi })$, wenn man als Belegung definiert:

$\beta _{k}^{\Phi }(v_{i})={\begin{cases}\,[v_{i}]_{\Phi },&{\mbox{wenn }}i<k\\\,[v_{0}]_{\Phi },&{\mbox{wenn }}i\geq k>0\\\,[c]_{\Phi },&{\mbox{wenn }}i\geq k=0\end{cases}}$

Terminterpretationen treten bei Herbrand-Strukturen und beim Satz von Henkin auf.