226 5 Modelltheorie
= TD(β, D, I, b'). Mit β, β* ∉ TT(Δ) gilt sodann auch b*FTT(A) = bFTT(A) = b'FTT(A)
und damit mit Theorem 5-6-(ii): D, I, b' к [β, ξ, Δ].
Zu (ii): Die R-L-Richtung ergibt sich direkt mit Theorem 5-4-(viii). Gelte nun fur die L-
R-Richtung D, I, b к rVξA^l. Dann gibt es ein β* ∈ PAR∖TT(Δ) und b*, das in β* Bele-
gungsvariante von b fur D, so dass D, I, b* к [β*, ξ, Δ]. Sei nun b' = (b∖{(β, b(β))}) ∪
{(β, b*(β*))}. Dann ist b' in β eine Belegungsvariante von b fur D und es ist TD(β*, D,
I, b*) = b*(β*) = b'(β) = TD(β, D, I, b'). Mit β, β* ∉ TT(Δ) gilt sodann auch wieder
b *FTT(A) = b TTT(A) und damit mit Theorem 5-6-(ii): D, I, b' к [β, ξ, Δ]. ■
Theorem 5-9. Einfaches Substitutionslemma fur Belegungen
Wenn (D, I) ein Modell, b eine Belegung fur D ist, ξ ∈ VAR, β ∈ PAR und θ ∈ GTERM,
dann:
(i) Wenn b’ in β eine Belegungsvariante von b fur D ist und bl(β) = TD(θ, D, I, b), dann
gilt fur alle θ+ ∈ TERM mit FV(θ+) ⊆ {ξ} und β ∉ TT(θ+): TD([θ, ξ, θ+], D, I, b) =
TD([β, ξ, θ+], D, I, b'), und
(ii) Wenn b' in β eine Belegungsvariante von b fur D ist und b'(β) = TD(θ, D, I, b), dann
gilt fur alle A ∈ FORM, wobei FV(A) ⊆ {ξ} und β ∉ TT(A): D, I, b к [θ, ξ, A] gdw
D, I, b1 к [β, ξ, A].
Beweis: Sei (D, I) ein Modell, b eine Belegung fur D, ξ ∈ VAR, β ∈ PAR und θ ∈
GTERM. Sei nun b' in β eine Belegungsvariante von b fur D, wobei b'(β) = TD(θ, D, I,
b). Sei nun μ ∈ TERM ∪ FORM mit FV(μ) ⊆ {ξ} und β ∉ TT(μ). Dann gilt trivialer-
weise I ΓTA(μ) = I FTA(μ). Sodann gilt mit β ∉ TT(μ), dass b ΓTT(μ) = b TTT(μ). Ferner
gilt nach Annahme: TD(β, D, I, b') = b'(β) = TD(θ, D, I, b).
Damit folgt nach Theorem 5-6-(i) fur alle θ+ ∈ TERM mit FV(θ+) ⊆ {ξ} und β ∉
TT(θ+): TD([θ, ξ, θ+], D, I, b) = TD([β, ξ, θ+], D, I, b') und mit Theorem 5-6-(ii) fur alle
A ∈ FORM, wobei FV(A) ⊆ {ξ} und β ∉ TT(A): D, I, b к [θ, ξ, A] gdw D, I, b` к [β,
ξ, A]. ■