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 L I S {\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 S {\displaystyle S} und eine Variablenbelegung gegeben. Wir beginnen mit der Festlegung des Universums der Interpretation. Durch

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

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

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

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

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

f T Φ : ( T Φ ) n T Φ , f T Φ ( [ t 1 ] Φ , , [ t n ] Φ ) := [ f t 1 t n ] Φ {\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 R {\displaystyle R}

R T Φ ( [ t 1 ] Φ , , [ t n ] Φ ) :⇔ Φ R t 1 t n {\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

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

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

Obigen Definitionen sieht man sofort an, dass durch

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

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

β k Φ ( v i ) = { [ v i ] Φ , wenn  i < k [ v 0 ] Φ , wenn  i k > 0 [ c ] Φ , wenn  i k = 0 {\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.

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.