Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

218   5 Modelltheorie

gdw

D, I', b' к Γ.

Zweitens: Sei Γ = ^rΑ ∧ Β^π. Also FGRAD(A) < FGRAD(Γ) und FGRAD(B) <
FGRAD(Γ). Dann ist nach Annahme fur Γ auch A, B ∈ GTERM, I((TA(A) ∪ TA(B)) =
I'((TA(A) ∪ TA(B)) und b((TT(A) ∪ TT(B)) = b'((TT(A) ∪ TT(B)). Mit Theorem
5-4-(iii) und I.V. gilt:

D, I, b к Γ
gdw

D, I, b к ^rA ∧ B¹
gdw

D, I, b к A und D, I, b к B
gdw

D, I', b' к A und D, I', b' к B
gdw

D, I', b' к rA ∧ B¹
gdw

D, I', b' к Γ.

Der dritte bis funfte Fall verlaufen analog.

Sechstens: Sei Γ = rΛζΔ^^l. Nach der Annahme fur Γ gilt dann FV(Δ) ⊆ {ζ}, I (TA(Δ) =
I'(TA(Δ) und b(TT(Δ) = b'(TT(Δ). Gelte nun D, I, b к rΛζΔ^^l. Dann gibt es mit
Theorem 5-4-(vii) ein β ∈ PAR∖TT(Δ), so dass fur alle b⁺, die in β Belegungsvarianten
von b fur D sind, gilt: D, I, b⁺ к [β, ζ, Δ]. Sei nun b'1 in β eine Belegungsvariante von
b' fur D. Sei nun b 1 = (b ∖{(β, b (β))}) ∪ {(β, b '1(β))}. Dann ist b 1 in β eine Belegungsva-
riante von b fur D und somit gilt: D, I, b 1 к [β, ζ, Δ]. Da β ∉ TT(Δ) gilt sodann mit
b(TT(Δ) = b'(TT(Δ) fur alle β' ∈ TT(Δ) ∩ PAR: b 1(β') = b(β') = b'(β') = b'1(β'). Da so-
dann auch b 1(β) = b '1(β) gilt damit wegen TT([β, ζ, Δ]) ⊆ TT(Δ) ∪ {β}, dass b 1(TT([β,
ζ, Δ]) = b'₁(([β, ζ, Δ]). Sodann gilt I(TA([β, ζ, Δ]) = I((TA([β, ζ, Δ]) ∩ (KONST ∪
FUNK ∪ PRA)) = I((TA(Δ) ∩ (KONST ∪ FUNK ∪ PRA)) = I(TA(Δ) = I'(TA(Δ) =
I'((TA(Δ) ∩ (KONST ∪ FUNK ∪ PRA)) = I^,((TA([β, ζ, Δ]) ∩ (KONST ∪ FUNK ∪
PRA)) = I'((TA([β, ζ, Δ]) und somit I(TA([β, ζ, Δ]) = I^l(TA([β, ζ, Δ]). Ferner ist [β, ζ, Δ]
∈ GFORM und mit Theorem 1-13 ist FGRAD([β, ζ, Δ]) = FGRAD(Δ) < FGRAD(Γ).
Damit gilt nach I.V. mit D, I, b 1 к [β, ζ, Δ] auch: D, I', b '1 к [β, ζ, Δ]. Also gilt fur alle

<<   189   190   191   192   193   194   195   >>

More intriguing information