Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

222   5 Modelltheorie

gdw

D, I', b' = [θ', ξ, ^r—A^π]

gdw

D, I', b' = [θ', ξ, Δ].

Zweitens: Sei Δ = ^rA ∧ B^π. Also FGRAD(A) < FGRAD(Δ) und FGRAD(B) <
FGRAD(Δ). Dann ist nach Annahme fur Δ auch FV(A) ∪ FV(B) ⊆ {ξ}, I((TA(A) ∪
TA(B)) = I'((TA(A) ∪ TA(B)) und b((TT(A) ∪ TT(B)) = b'((TT(A) ∪ TT(B)). Mit I.V.
und Theorem 5-4-(iii) gilt dann:

D, I, b = [θ, ξ, Δ]

gdw

D, I, b = [θ, ξ, ^γa ∧ Bη

D, I, b = ^r[θ, ξ, A] ∧ [θ, ξ, BΓ

D, I, b = [θ, ξ, A] und D, I, b = [θ, ξ, B]
gdw

D, I', b' = [θ`, ξ, A] und D, I', b' = [θ', ξ, B]

D, I', b' = ^r[θ', ξ, A] ∧ [θ', ξ, BΓ

gdw

D, I^,, b' = [θ', ξ, ^γa ∧ Bη
gdw

D, I', b' = [θ', ξ, Δ].

Der dritte bis funfte Fall verlaufen analog.

Sechstens: Sei Δ = ^rΛζA^^l. Nach der Annahme fur Δ ist dann FV(A) ⊆ {ξ, ζ}, I (TA(A)
= I ^l(TA(A) und b (TT(A) = b ^l(TT(A). Angenommen ζ = ξ. Dann ist [θ, ξ, Δ] = [θ, ζ,
^rΛζA^^l ] = ^rΛζA^^l = [θ', ζ, ^rΛζA^^l ] = [θ', ξ, Δ] und somit [θ, ξ, Δ] = Δ = [θ', ξ, Δ]. Sodann
gilt FV(Δ) = 0 und somit Δ ∈ GFORM. Da nach Annahme I(TA(Δ) = I^l(TA(Δ) und
b (TT(Δ) = b ^l(TT(Δ) gilt damit mit Theorem 5-5-(ii): D, I, b = [θ, ξ, Δ] gdw D, I, b = Δ
gdw D, I^,, b' = Δ gdw D, I^,, b' = [θ', ξ, Δ]. Sei nun ζ ≠ ξ. Dann ist [θ, ξ, Δ] = ^rΛζ[θ, ξ,
A]^π und [θ', ξ, Δ] = ^rΛζ[θ^,, ξ, A]^π. Sodann gilt mit ζ ≠ ξ und ζ, ξ ∉ TT(θ*) fur alle θ# ∈
GTERM nach Theorem 1-25-(ii) fur alle β⁺ ∈ PAR: [β⁺, ζ, [θ, ξ, A]] = [θ, ξ, [β⁺, ζ, A]]
und [β⁺, ζ, [θ', ξ, A]] = [θ', ξ, [β⁺, ζ, A]].

<<   <   193   194   195   196   197   198   199   >   >>