Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

224   5 Modelltheorie

Siebtens: Sei Δ = ^rVζΑ^^l. Nach der Annahme fur Δ ist dann FV(Α) ⊆ {ξ, ζ}, I ΓTA(A) =
I'tTA(Λ) und bΓTT(A) = b'ΓTT(A). Angenommen ζ = ξ. Dann ist [θ, ξ, Δ] = [θ, ζ,
^rVζA^π] = ^rVζA^π = [θ', ζ, ^rVζA^π] = [θ', ξ, Δ] und somit [θ, ξ, Δ] = Δ = [θ', ξ, Δ]. Sodann
gilt FV(Δ) = 0 und somit Δ ∈ GFORM. Da nach Annahme IΓTA(Δ) = I'ΓTA(Δ) und
bΓTT(Δ) = b'Γ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 [θ, ξ, Δ] = ^rVζ[θ, ξ,
A]^π und [θ', ξ, Δ] = ^rVζ[θ', ξ, A]^π. Sodann gilt mit ζ ≠ ξ und ζ, ξ ∉ TT(θ*) fur alle θ# ∈
GTERM nach Theorem 1-25-(ii) fur alle β⁺ ∈ PAR: [β⁺, ζ, [θ, ξ, Λ]] = [θ, ξ, [β⁺, ζ, Λ]]
und [β⁺, ζ, [θ', ξ, Λ]] = [θ', ξ, [β⁺, ζ, Λ]].

Gelte nun D, I, b к ^rVζ[θ, ξ, A]^^l. Dann gibt es mit Theorem 5-4-(viii) ein β⁺ ∈
PAR∖TT([θ, ξ, Λ]) und b ₁, das in β⁺ Belegungsvariante von b fur D ist, so dass D, I, b 1
к [β⁺, ζ, [θ, ξ, A]]. Sei nun в# ∈ PAR∖(TT([θ, ξ, Λ]) ∪ TT(θ) ∪ TT(θ')). Sei nun b'1 =
(b '\{(в#, b '(в#))}) ∪ {(в#, b 1(β⁺))}. Dann ist b '1 in в# eine Belegungsvariante von b' fur
D und b’1(P#) = b 1(β⁺). Sei nun b2 = (b\{(в#, b(в#))}) ∪ {(в#, b’1(в#))}. Dann ist b2 in в#
eine Belegungsvariante von b fur D und ТО(в#, D, I, b₂) = b₂(в#) = b'1(в#) = b 1(в⁺) =
TDφ⁺, D, I, b 1). Sodann gilt nach Annahme fur в⁺, в#, dass в⁺, в# ∉ TT([θ, ξ, A]) und
damit b₂ΓTT([θ, ξ, A]) = bΓTT([θ, ξ, A]) = b 1fTT([θ, ξ, Λ]). Sodann ist trivialerweise
IΓTA([θ, ξ, A]) = IΓTA([θ, ξ, A]). Ferner ist FV([θ, ξ, A]) ⊆ {ζ} und mit Theorem 1-13
ist FGRAD([θ, ξ, A]) = FGRAD(A) < FGRAD(Δ). Damit gilt mit D, I, b 1 к [в⁺, ζ, [θ, ξ,
Λ]] nach I.V., dass D, I, b 2 к [в#, ζ, [θ, ξ, A]] = [θ, ξ, [в#, ζ, A]].

Sodann ist mit в# ∉ TT(θ) und в# ∉ TT(θ'): b2ΓTT(θ) = bΓTT(θ) und b'1ΓTT(θ') =
b 'ΓTT(θ') und somit nach Theorem 5-5-(i) TD(θ, D, I, b ₂) = TD(θ, D, I, b) und TD(θ',
D, I', b'1) = TD(θ', D, I', b') und somit nach Eingangsannahme insgesamt TD(θ, D, I,
b2) = TD(θ', D, I', b'1). Ferner gilt mit b ΓTT(A) = bTTT(A), b₂(в#) = b'1(в#) und ТТ([в#,
ζ, A]) ⊆ TT(A) ∪ {в#}, dass b2ΓTT(^, ζ, A]) = b’1Г([в^#, ζ, A]) und es gilt IΓTA(^, ζ,
A]) = IГ(ТЛ([в^#, ζ, A]) ∩ (KONST ∪ FUNK ∪ PRA)) = IΓ(TA(A) ∩ (KONST ∪ FUNK
∪ PRA)) = IΓTA(A) = I'ΓTA(A) = I'Γ(TA(A) ∩ (KONST ∪ FUNK ∪ PRA)) =
I'Γ(TA(^, ζ, A]) ∩ (KONST ∪ FUNK ∪ PRA)) = I'Γ(TA(^, ζ, A]) und somit IΓTA(^,
ζ, A]) = I'ΓTA(^, ζ, A]). Ferner ist FV(∣β*, ζ, A]) ⊆ {ξ} und mit Theorem 1-13 ist

<<   <   195   196   197   198   199   200   201   >   >>