Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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θ = θ¹.

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θ = θ^π. ■

<<   207   208   209   210   211   212   213   >>

More intriguing information