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 <math>\Phi</math> von Ausdrücken einer Sprache <math>L_I^S</math> gegeben, so soll eine von <math>\Phi</math> 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 <math>S</math> und eine Variablenbelegung gegeben. Wir beginnen mit der Festlegung des Universums der Interpretation. Durch

<math>t_1 \sim t_2 \quad \Leftrightarrow \quad \Phi \vdash t_1\equiv t_2 </math>

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

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

<math>c^{{\mathcal T}^\Phi}\quad := \quad [c]_\Phi \in T^\Phi</math>.

Für ein n-stelliges Funktionssymbol <math>f</math> definiere

<math>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</math>

und für ein n-stelliges Relationssymbol <math>R</math>

<math>R^{{\mathcal T}^\Phi}([t_1]_\Phi,\ldots,[t_n]_\Phi)\quad :\Leftrightarrow \quad \Phi \vdash Rt_1\ldots t_n</math>.

Man kann zeigen, dass diese Festlegungen wohldefiniert sind. Schließlich ist noch eine Variablenbelegung <math>\beta^\Phi</math> anzugeben; man setzt einfach

<math>\beta^\Phi(v_i) \,:=\, [v_i]_\Phi</math>, wobei <math>v_0, v_1, v_2, \ldots</math> die Variablen seien.

Insgesamt ist dadurch die sogenannte Terminterpretation <math>{\mathcal T}^\Phi = (T^\Phi, \beta^\Phi)</math> definiert<ref>Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik. Spektrum Akademischer Verlag, Heidelberg/Berlin/Oxford 1996, ISBN 3-8274-0130-5, insbesondere Kapitel V, § 1.</ref>.

Obigen Definitionen sieht man sofort an, dass durch

<math>T_k^\Phi := \{[t]_\Phi;\, t\in T, \mathrm{var}(t) \subset \{v_0,\ldots v_{k-1}\}\} </math>

Unterstrukturen definiert sind, wobei <math>\mathrm{var}(t)</math> für die Menge der im Term <math>t</math> vorkommenden Variablen steht und die Symbolmenge im Falle <math>k=0</math> wenigstens ein Konstantensymbol <math>c</math> enthalten muss, damit <math>T_k^\Phi</math> nicht leer ist<ref>Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Einführung in die mathematische Logik. Spektrum Akademischer Verlag, Heidelberg/Berlin/Oxford 1996, ISBN 3-8274-0130-5, insbesondere Kapitel XI, § 1.</ref>. Man erhält so weitere Interpretationen <math>{\mathcal T}_k^\Phi = (T_k^\Phi, \beta_k^\Phi)</math>, wenn man als Belegung definiert:

<math>\beta_k^\Phi(v_i)=\begin{cases} \,[ v_i ]_\Phi, & \mbox{wenn } i < k \\ \,[v_0]_\Phi, & \mbox{wenn } i \ge k > 0 \\ \,[c]_\Phi, & \mbox{wenn } i \ge k = 0 \end{cases}</math>

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

Einzelnachweise