5.1 Erfullungsrelation und modelltheoretische Konsequenz 213
Definition 5-5. Termdenotationsfunktionen fur Modelle und Belegungen
F ist eine Termdenotationsfunktion fur D, I, b
gdw
(D, I) ist ein Modell und b eine Belegung fur D und F ist eine Funktion auf GTERM und:
(i) Wenn α ∈ KONST, dann F (α) = I (α),
(ii) Wenn β ∈ PAR, dann F (β) = b (β), und
(iii) Wenn φ ∈ FUNK und φ r-stellig ist und θ0, ..., θr-1 ∈ GTERM, dann
F(rφ(θo, ..., θr,ɪ)ɔ) = I(φ)(<F(θo), ..., F(θ,4)>).
Theorem 5-1. Fur jedes Modell (D, I) und Belegung b fur D gibt es genau eine Termdenota-
tionsfunktion
Wenn (D, I) ein Modell und b eine Belegung fur D ist, dann gibt es genau ein F, so dass F
eine Termdenotationsfunktion fur D, I, b ist.
Beweis: Sei (D, I) ein Modell und b eine Belegung fur D. Dann gibt es mit den Theore-
men uber eindeutige Lesbarkeit (Theorem ɪ-ɪ0 und Theorem ɪ-ɪɪ) genau eine Funktion
F auf GTERM, so dass Klauseln (i) bis (iii) von Definition 5-5 fur F erfullt sind und da-
mit nach Definition 5-5 genau eine Termdenotationsfunktion fur D, I, b. ■
Definition 5-6. Termdenotationsoperation (TD)
TD(θ, D, I, b) = a
gdw
(i) Es gibt eine Termdenotationsfunktion F fur D, I, b und θ ∈ GTERM und a = F(θ)
oder
(ii) Es gibt keine Termdenotationsfunktion fur D, I, b oder θ ∉ GTERM und a = 0.
Das folgende Theorem spiegelt die ubliche Definition von Termdenotaten fur Modelle
und Belegungen wider: