216 5 Modelltheorie
es mit Theorem 5-3 genau eine Erfullungsfunktion F fur D, I. Damit gilt dann mit
Definition 5-8 fur alle Γ ∈ GFORM: D, I, b к Γ gdw F(Γ, b) = 1 und D, I, b ≠ Γ gdw
F(Γ, b) = 0. Daraus ergibt sich die Behauptung dann mit Definition 5-7. ■
Theorem 5-5. Koinzidenzlemma
Wenn (D, I) und (D, I') Modelle und b, b' Belegungen fur D sind, dann:
(i) Fur alle θ ∈ GTERM: Wenn I ΓTA(θ) = I 'ΓTA(θ) und b ΓTT(θ) = b 'ΓTT(θ), dann TD(θ,
D, I, b) = TD(θ, D, I', b'), und
(ii) Fur alle Γ ∈ GFORM: Wenn I ΓTA(Γ) = I 'ΓTA(Γ) und b ΓTT(Γ) = b 'ΓTT(Γ), dann D,
I, b к Γ gdw D, I', b' к Γ.
Beweis: Zu (i): Seien (D, I) und (D, I') Modelle und b, b' Belegungen fur D. Der Beweis
wird durch Induktion uber den Termaufbau von θ ∈ TERM gefuhrt. Sei zunachst θ ∈
ATERM ∩ GTERM und gelte IΓTA(θ) = I'ΓTA(θ) und bΓTT(θ) = b'ΓTT(θ). Dann ist θ ∈
KONST ∪ PAR. Sei nun θ ∈ KONST. Dann gilt mit {θ} = TA(θ) ∩ KONST, I ΓTA(θ) =
I'ΓTA(θ) und Theorem 5-2-(i): TD(θ, D, I, b) = I(θ) = I'(θ) = TD(θ, D, I', b'). Sei nun θ
∈ PAR. Dann gilt mit {θ} = TT(θ) ∩ PAR, b ΓTT(θ) = b 'ΓTT(θ) und Theorem 5-2-(ii):
TD(θ, D, I, b) = b(θ) = b'(θ) = TD(θ, D, I', b').
Gelte die Behauptung nun fur θ0, ., θr-ι ∈ TERM und sei φ ∈ FUNK, wobei φ r-
stellig, und sei rφ(θo, ., θr-ι)π ∈ FTERM ∩ GTERM und gelte I ΓTA(rφ(θo, ., θr-ι)π) =
I TTA(rφ(θo, ., θr-ι)π) und b ΓTT(rφ(θo, ., θr-ɪ)ɔ) = b TTT(rφ(θo, ., θr-ι)π). Dann gilt
mit FV(rφ(θ0, ., θr-ι)^l) = U{FV(θi) | i < r} fur alle θi mit i < r ebenfalls: θi ∈ GTERM.
Sodann gilt mit U{TA(θi) | i < r} ⊆ TA(rφ(θ0, ., θr-ι)^l) und U{TT(θi) | i < r} ⊆
TT(rφ(θo, ., θr-ι)π) fur alle i < r: I ΓTA(θi) = I 'ΓTA(θi) und b ΓTT(θi) = b 'ΓTT(θi). Mit
I.V. gilt somit fur alle i < r: TD(θi, D, I, b) = TD(θi, D, I', b'). Sodann gilt mit φ ∈
TA(rφ(θ0, ., θr-ι)^l) ∩ FUNK nach Annahme auch I (φ) = I '(φ). Damit gilt:
TD(rφ(θo, ., θr-ʃ, D, I, b)
I(φ)((TD(θo, D, I, b), ., TD(θr-ι, D, I, b)>)
I'(φ)((TD(θo, D, I', b'), ., TD(θr-ι, D, I, b')>)
TD(rφ(θo, ., θr-ʃ, D, I', b').