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 Φ von Ausdrücken einer Sprache $L_I^S$ gegeben, so soll eine von Φ 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 / ∼ 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 β^Φ 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^[1].

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 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^[2]. 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 \ge k > 0 \\ \,[c]_\Phi, & \mbox{wenn } i \ge k = 0 \end{cases}$

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

Einzelnachweise

1. ↑ 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.
2. ↑ 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.