Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

5.1 Erfullungsrelation und modelltheoretische Konsequenz 219

b'⁺ die in β Belegungsvarianten von b' fur D sind: D, I', b'⁺ к [β, ζ, Δ] und somit nach
Theorem 5-4-(vii) D, I', b` к ^rΛζΔ^^l. Die R-L-Richtung verlauft analog.

Siebtens: Sei Γ = ^rVζΔ^^l. Nach der Annahme fur Γ ist dann FV(Δ) ⊆ {ζ}, I ΓTA(Δ) =
I'ΓTA(Δ) und b ΓTT(Δ) = b'ΓTT(Δ). Gelte nun D, I, b к ^rVζΔ^^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 ₁ к [β, ζ, Δ]. Sei nun b '₁ = (b '∖{(β, b '(β))}) ∪ {(β, b ₁(β))}. Dann ist b '₁
in β eine Belegungsvariante von b' fur D. Da β ∉ TT(Δ) gilt sodann mit bΓTT(Δ) =
b'ΓTT(Δ) fur alle β' ∈ TT(Δ) ∩ PAR: bι(β') = b(β') = b'(β') = b'ι(β'). Da sodann auch
bι(β) = b∙₁(β) gilt weiter mit TT([β, ζ, Δ]) ⊆ TT(Δ) ∪ {β}, dass b ₁∏T([β, ζ, Δ]) =
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'ΓTA([β, ζ, Δ]). Ferner ist [β, ζ, Δ] ∈
GFORM und mit Theorem 1-13 ist FGRAD([β, ζ, Δ]) = FGRAD(Δ) < FGRAD(Γ). Damit
gilt nach I.V. mit D, I, b ₁ к [β, ζ, Δ] auch: D, I^l, b ^l₁ к [β, ζ, Δ] und somit nach Theorem
5-4-(viii) D, I^l, b ` к ^rVζΔ^^l. Die R-L-Richtung verlauft analog. ■

Mit Hilfe des Koinzidenzlemmas kann nun das Substitutionslemma bewiesen werden:

Theorem 5-6. Substitutionslemma

Wenn (D, I), (D, I') Modelle, b, b' Belegungen fur D sind, ξ ∈ VAR, θ, θ' ∈ GTERM und
TD(θ, D, I, b) = TD(θ', D, I', b') dann:

(i) Fur alle θ⁺ ∈ TERM mit FV(θ⁺) ⊆ {ξ}, IΓTA(θ⁺) = I'ΓTA(θ⁺) und bΓTT(θ⁺) =
b 'ΓTT(θ) gilt: TD([θ, ξ, θ⁺], D, I, b) = TD([θ', ξ, θ⁺], D, I', b'), und

(ii) Fur alle Δ ∈ FORM mit FV(Δ) ⊆ {ξ}, I ΓTA(Δ) = I ^,ΓTA(Δ) und b ΓTT(Δ) = b ^,ΓTT(Δ)
gilt: D, I, b к [θ, ξ, Δ] gdw D, I', b' к [θ', ξ, Δ].

Beweis: Zu (i): Seien (D, I), (D, I') Modelle, b, b' Belegungen fur D, ξ ∈ VAR, θ, θ' ∈
GTERM und TD(θ, D, I, b) = TD(θ', D, I', b'). Der Beweis wird mittels Induktion uber
den Termaufbau von θ⁺ ∈ TERM gefuhrt. Sei zunachst θ⁺ ∈ ATERM, wobei FV(θ⁺) ⊆
{ξ}, I ΓTA(θ⁺) = I 'ΓTA(θ⁺) und b ΓTT(θ⁺) = b 'ΓTT(θ⁺). Dann ist θ⁺ ∈ KONST ∪ PAR ∪
VAR. Sei nun θ⁺ ∈ KONST. Dann ist [θ, ξ, θ⁺] = θ⁺ = [θ', ξ, θ⁺] und damit gilt mit TA(θ⁺)

<<   190   191   192   193   194   195   196   >>

More intriguing information