5.1 Erfullungsrelation und modelltheoretische Konsequenz 219
b'+ die in β Belegungsvarianten von b' fur D sind: D, I', b'+ к [β, ζ, Δ] und somit nach
Theorem 5-4-(vii) D, I', b` к rΛζΔ^l. Die R-L-Richtung verlauft analog.
Siebtens: Sei Γ = rVζΔ^l. Nach der Annahme fur Γ ist dann FV(Δ) ⊆ {ζ}, I ΓTA(Δ) =
I'ΓTA(Δ) und b ΓTT(Δ) = b'ΓTT(Δ). Gelte nun D, I, b к rVζΔ^l. Dann gibt es mit
Theorem 5-4-(viii) ein β ∈ PAR∖TT(Δ) und b 1, das in β Belegungsvariante von b fur D
ist, so dass D, I, b 1 к [β, ζ, Δ]. Sei nun b '1 = (b '∖{(β, b '(β))}) ∪ {(β, b 1(β))}. Dann ist b '1
in β eine Belegungsvariante von b' fur D. Da β ∉ TT(Δ) gilt sodann mit bΓTT(Δ) =
b'ΓTT(Δ) fur alle β' ∈ TT(Δ) ∩ PAR: bι(β') = b(β') = b'(β') = b'ι(β'). Da sodann auch
bι(β) = b∙1(β) gilt weiter mit TT([β, ζ, Δ]) ⊆ TT(Δ) ∪ {β}, dass b 1∏T([β, ζ, Δ]) =
b,ιΓ([β, ζ, Δ]). Sodann gilt IΓTA([β, ζ, Δ]) = IΓ(TA([β, ζ, Δ]) ∩ (KONST ∪ FUNK ∪
PRA)) = I Γ(TA(Δ) ∩ (KONST ∪ FUNK ∪ PRA)) = I ΓTA(Δ) = I 'ΓTA(Δ) = I 'Γ(TA(Δ) ∩
(KONST ∪ FUNK ∪ PRA)) = I'Γ(TA([β, ζ, Δ]) ∩ (KONST ∪ FUNK ∪ PRA)) =
I'Γ(TA([β, ζ, Δ]) und somit IΓTA([β, ζ, Δ]) = I'ΓTA([β, ζ, Δ]). Ferner ist [β, ζ, Δ] ∈
GFORM und mit Theorem 1-13 ist FGRAD([β, ζ, Δ]) = FGRAD(Δ) < FGRAD(Γ). Damit
gilt nach I.V. mit D, I, b 1 к [β, ζ, Δ] auch: D, Il, b l1 к [β, ζ, Δ] und somit nach Theorem
5-4-(viii) D, Il, b ` к rVζΔ^l. Die R-L-Richtung verlauft analog. ■
Mit Hilfe des Koinzidenzlemmas kann nun das Substitutionslemma bewiesen werden:
Theorem 5-6. Substitutionslemma
Wenn (D, I), (D, I') Modelle, b, b' Belegungen fur D sind, ξ ∈ VAR, θ, θ' ∈ GTERM und
TD(θ, D, I, b) = TD(θ', D, I', b') dann:
(i) Fur alle θ+ ∈ TERM mit FV(θ+) ⊆ {ξ}, IΓTA(θ+) = I'ΓTA(θ+) und bΓTT(θ+) =
b 'ΓTT(θ) gilt: TD([θ, ξ, θ+], D, I, b) = TD([θ', ξ, θ+], D, I', b'), und
(ii) Fur alle Δ ∈ FORM mit FV(Δ) ⊆ {ξ}, I ΓTA(Δ) = I ,ΓTA(Δ) und b ΓTT(Δ) = b ,ΓTT(Δ)
gilt: D, I, b к [θ, ξ, Δ] gdw D, I', b' к [θ', ξ, Δ].
Beweis: Zu (i): Seien (D, I), (D, I') Modelle, b, b' Belegungen fur D, ξ ∈ VAR, θ, θ' ∈
GTERM und TD(θ, D, I, b) = TD(θ', D, I', b'). Der Beweis wird mittels Induktion uber
den Termaufbau von θ+ ∈ TERM gefuhrt. Sei zunachst θ+ ∈ ATERM, wobei FV(θ+) ⊆
{ξ}, I ΓTA(θ+) = I 'ΓTA(θ+) und b ΓTT(θ+) = b 'ΓTT(θ+). Dann ist θ+ ∈ KONST ∪ PAR ∪
VAR. Sei nun θ+ ∈ KONST. Dann ist [θ, ξ, θ+] = θ+ = [θ', ξ, θ+] und damit gilt mit TA(θ+)