236 5 Modelltheorie
Theorem 5-30. Modelltheoretische Entsprechung zu PB
Wenn β ∈ PAR, ξ ∈ VAR, Α ∈ FORM, wobei FV(Α) ⊆ {ξ}, und X к rVξΑπ und Y к Β und
{[β, ξ, Α]} ∈ Y und β ∉ TTFM((Y{[β, ξ, Α]}) ∪ {Α, Β}), dann X ∪ (Y{[β, ξ, Α]}) к Β.
Beweis: Seien β ∈ PAR, ξ ∈ VAR, Α ∈ FORM, wobei FV(Α) ⊆ {ξ}, X к rVξΑπ, Y к
Β, {[β, ξ, Α]} ∈ Y und β ∉ TTFM((Y∖{[β, ξ, Α]}) ∪ {Α, Β}). Sei D, I, b к X ∪ (Y∖{[β,
ξ, Α]}). Dann ist (D, I) ein Modell und b eine Belegung fur D und mit Theorem 5-10 gilt
D, I, b к X und D, I, b к Y∖{[β, ξ, Α]}. Nach Voraussetzung gilt dann auch D, I, b к
rVξΑ^l. Da β ∉ TT(Α), gibt es dann nach Theorem 5-8-(ii) ein b', das in β eine Bele-
gungsvariante von b fur D ist, so dass D, I, b` к [β, ξ, Α]. Sei nun Δ' ∈ Y, also Δ' ∈
Y∖{[β, ξ, Α]} oder Δ' = [β, ξ, Α]. Im ersten Fall gilt D, I, b к Δ'. Da aber β ∉ TT(Δ'), gilt
bFTT(Δ,) = b,∣'TT(Δ'). Mit Theorem 5-5-(ii) folgt dann D, I, b' к Δ'. Fur den zweiten
Fall gilt bereits D, I, b' к [β, ξ, Α]. Also D, I, b' к Δ' fur alle Δ' ∈ Y und somit D, I, b'
к Y. Nach Voraussetzung gilt dann auch D, I, b' к Β. Da aber β ∉ TT(Β), gilt b ΓTT(Β)
= b,∣'TT(Β). Mit Theorem 5-5-(ii) folgt dann D, I, b к Β. Also gilt fur alle D, I, b:
Wenn D, I, b к X ∪ (Y∖{[β, ξ, Α]}), dann D, I, b к Β. Also X ∪ (Y∖{[β, ξ, Α]}) к Β.
■
Theorem 5-31. Modelltheoretische Entsprechung zu IE
Fur alle X ⊆ GFORM und θ ∈ GTERM gilt: X к rθ = θ1.
Beweis: Sei X ⊆ GFORM und θ ∈ GTERM. Gelte D, I, b к X. Dann ist (D, I) ein Mo-
dell und b eine Belegung fur D. Mit (TD(θ, D, I, b), TD(θ, D, I, b)) ∈ {(a, a) | a ∈ D}
gilt (TD(θ, D, I, b), TD(θ, D, I, b)) ∈ I(r=^l). Nach Theorem 5-4-(i) gilt dann D, I, b к
rθ = θ^l. Also gilt fur alle D, I, b: Wenn D, I, b к X, dann D, I, b к rθ = θ^l. Also X к
rθ = θπ. ■