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 ${\displaystyle \Phi }$ von Ausdrücken einer Sprache ${\displaystyle L_{I}^{S}}$ gegeben, so soll eine von ${\displaystyle \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 ${\displaystyle S}$ und eine Variablenbelegung gegeben. Wir beginnen mit der Festlegung des Universums der Interpretation. Durch

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

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

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

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

Für ein n-stelliges Funktionssymbol ${\displaystyle f}$ definiere

${\displaystyle 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 ${\displaystyle R}$

${\displaystyle 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 ${\displaystyle \beta ^{\Phi }}$ anzugeben; man setzt einfach

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

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

Obigen Definitionen sieht man sofort an, dass durch

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

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

${\displaystyle \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.