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 $\mathrm{\Phi }$ von Ausdrücken einer Sprache $L_I^S$ gegeben, so soll eine von $\mathrm{\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\iff \mathrm{\Phi }⊢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^{\mathrm{\Phi }}$ bezeichnet, die Äquivalenzklasse eines Terms mit $[t{]}_{\mathrm{\Phi }}$. Wir verwenden $T^{\mathrm{\Phi }}$ als Universum einer Interpretation ${𝒯}^{\mathrm{\Phi }}$.

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

$c^{{𝒯}^{\mathrm{\Phi }}}:=[c{]}_{\mathrm{\Phi }}\in T^{\mathrm{\Phi }}$.

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

$f^{{𝒯}^{\mathrm{\Phi }}}:(T^{\mathrm{\Phi }}{)}^n\to T^{\mathrm{\Phi }},f^{{𝒯}^{\mathrm{\Phi }}}([t_1{]}_{\mathrm{\Phi }},\dots ,[t_n{]}_{\mathrm{\Phi }}):=[f{t}_1\dots t_n{]}_{\mathrm{\Phi }}$

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

$R^{{𝒯}^{\mathrm{\Phi }}}([t_1{]}_{\mathrm{\Phi }},\dots ,[t_n{]}_{\mathrm{\Phi }}):\iff \mathrm{\Phi }⊢R{t}_1\dots t_n$.

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

${\beta }^{\mathrm{\Phi }}(v_i):=[v_i{]}_{\mathrm{\Phi }}$, wobei $v_0,v_1,v_2,\dots$ die Variablen seien.

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

Obigen Definitionen sieht man sofort an, dass durch

$T_k^{\mathrm{\Phi }}:=\{[t{]}_{\mathrm{\Phi }};t\in T,\mathrm{v}\mathrm{a}\mathrm{r}(t)\subset \{v_0,\dots v_{k-1}\}\}$

Unterstrukturen definiert sind, wobei $\mathrm{v}\mathrm{a}\mathrm{r}(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^{\mathrm{\Phi }}$ nicht leer ist. Man erhält so weitere Interpretationen ${𝒯}_k^{\mathrm{\Phi }}=(T_k^{\mathrm{\Phi }},{\beta }_k^{\mathrm{\Phi }})$, wenn man als Belegung definiert:

${\beta }_k^{\mathrm{\Phi }}(v_i)=\{\begin{array}{cc}[v_i{]}_{\mathrm{\Phi }},& \text{wenn }i<k\\ [v_0{]}_{\mathrm{\Phi }},& \text{wenn }i\ge k>0\\ [c{]}_{\mathrm{\Phi }},& \text{wenn }i\ge k=0\end{array}$

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