5.2 Abgeschlossenheit der modelltheoretischen Konsequenzschaft 235
b = rΛξΑ^l. Also gilt fur alle D, I, b: Wenn D, I, b = X, dann auch D, I, b к rΛξΑ^l.
Also X = rΛξΑ^l. ■
Theorem 5-28. Modelltheoretische Entsprechung zu UB
Wenn θ ∈ GTERM, ξ ∈ VAR, Α ∈ FORM, wobei FV(Α) ⊆ {ξ}, und X = rΛξΑ"1, dann X =
[θ, ξ, Α].
Beweis: Sei θ ∈ GTERM, ξ ∈ VAR, Α ∈ FORM, wobei FV(Α) ⊆ {ξ}, und X = rΛξΑπ.
Sei D, I, b = X. Dann ist (D, I) ein Modell und b eine Belegung fur D und nach Vo-
raussetzung gilt D, I, b = rΛξΑ^l. Dann gibt es nach Theorem 5-4-(vii) ein β ∈
PAR∖TT(Α), so dass fur alle b', die in β eine Belegungsvariante von b fur D sind, gilt D,
I, b` = [β, ξ, Α]. Sei b* = (b∖{(β, b(β))}) ∪ {(β, TD(θ, D, I, b))}. Offenbar ist b* in β
eine Belegungsvariante von b fur D. Also D, I, b* = [β, ξ, Α]. Mit b*(β) = TD(θ, D, I,
b) und β ∉ TT(Α) folgt dann mit Theorem 5-9-(ii), dass D, I, b = [θ, ξ, Α]. Also gilt fur
alle D, I, b: Wenn D, I, b = X, dann D, I, b = [θ, ξ, Α]. Also X = [θ, ξ, Α]. ■
Theorem 5-29. Modelltheoretische Entsprechung zu PE
Wenn θ ∈ GTERM, ξ ∈ VAR, Α ∈ FORM, wobei FV(Α) ⊆ {ξ}, und X = [θ, ξ, Α], dann X
= rVξΑπ.
Beweis: Sei θ ∈ GTERM, ξ ∈ VAR, Α ∈ FORM, wobei FV(Α) ⊆ {ξ}, und X = [θ, ξ,
Α]. Sei D, I, b = X. Dann ist (D, I) ein Modell und b eine Belegung fur D und nach
Voraussetzung gilt D, I, b = [θ, ξ, Α]. Sei nun β ∈ PAR∖TT(Α) und sei b * = (b ∖{(β,
b(β))}) ∪ {(β, TD(θ, D, I, b))}. Dann ist b* in β eine Belegungsvariante von b fur D.
Mit b *(β) = TD(θ, D, I, b), β ∉ TT(Α) und Theorem 5-9-(ii) folgt dann D, I, b * = [β, ξ,
Α]. Mit Theorem 5-4-(viii) folgt damit dann D, I, b = rVξΑ^l. Also gilt fur alle D, I, b:
Wenn D, I, b = X, dann D, I, b = rVξΑπ. Also X = rVξΑπ. ■