Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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ΛξΑ"¹, 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ξΑ^π. ■

<<   206   207   208   209   210   211   212   >>

More intriguing information