Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

226   5 Modelltheorie

= TD(β, D, I, b'). Mit β, β* ∉ TT(Δ) gilt sodann auch b*FTT(A) = bFTT(A) = b'FTT(A)
und damit mit Theorem 5-6-(ii): D, I, b' к [β, ξ, Δ].

Zu (ii): Die R-L-Richtung ergibt sich direkt mit Theorem 5-4-(viii). Gelte nun fur die L-
R-Richtung D, I, b к ^rVξA^^l. Dann gibt es ein β* ∈ PAR∖TT(Δ) und b*, das in β* Bele-
gungsvariante von b fur D, so dass D, I, b* к [β*, ξ, Δ]. Sei nun b' = (b∖{(β, b(β))}) ∪
{(β, b*(β*))}. Dann ist b' in β eine Belegungsvariante von b fur D und es ist TD(β*, D,
I, b*) = b*(β*) = b'(β) = TD(β, D, I, b'). Mit β, β* ∉ TT(Δ) gilt sodann auch wieder
b *FTT(A) = b TTT(A) und damit mit Theorem 5-6-(ii): D, I, b' к [β, ξ, Δ]. ■

Theorem 5-9. Einfaches Substitutionslemma fur Belegungen

Wenn (D, I) ein Modell, b eine Belegung fur D ist, ξ ∈ VAR, β ∈ PAR und θ ∈ GTERM,
dann:

(i)   Wenn b’ in β eine Belegungsvariante von b fur D ist und b^l(β) = TD(θ, D, I, b), dann

gilt fur alle θ⁺ ∈ TERM mit FV(θ⁺) ⊆ {ξ} und β ∉ TT(θ⁺): TD([θ, ξ, θ⁺], D, I, b) =

TD([β, ξ, θ⁺], D, I, b'), und

(ii)   Wenn b' in β eine Belegungsvariante von b fur D ist und b'(β) = TD(θ, D, I, b), dann

gilt fur alle A ∈ FORM, wobei FV(A) ⊆ {ξ} und β ∉ TT(A): D, I, b к [θ, ξ, A] gdw

D, I, b¹ к [β, ξ, A].

Beweis: Sei (D, I) ein Modell, b eine Belegung fur D, ξ ∈ VAR, β ∈ PAR und θ ∈
GTERM. Sei nun b' in β eine Belegungsvariante von b fur D, wobei b'(β) = TD(θ, D, I,
b). Sei nun μ ∈ TERM ∪ FORM mit FV(μ) ⊆ {ξ} und β ∉ TT(μ). Dann gilt trivialer-
weise I ΓTA(μ) = I FTA(μ). Sodann gilt mit β ∉ TT(μ), dass b ΓTT(μ) = b TTT(μ). Ferner
gilt nach Annahme: TD(β, D, I, b') = b'(β) = TD(θ, D, I, b).

Damit folgt nach Theorem 5-6-(i) fur alle θ⁺ ∈ TERM mit FV(θ⁺) ⊆ {ξ} und β ∉
TT(θ⁺): TD([θ, ξ, θ⁺], D, I, b) = TD([β, ξ, θ⁺], D, I, b') und mit Theorem 5-6-(ii) fur alle
A ∈ FORM, wobei FV(A) ⊆ {ξ} und β ∉ TT(A): D, I, b к [θ, ξ, A] gdw D, I, b` к [β,
ξ, A]. ■

<<   197   198   199   200   201   202   203   >>

More intriguing information