Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

220   5 Modelltheorie

= {θ⁺}, IΓTA(θ⁺) = I'ΓTA(θ⁺) und Theorem 5-2-(i): TD([θ, ξ, θ⁺], D, I, b) = TD(θ⁺, D, I,
b) = I(θ⁺) = I'(θ⁺) = TD(θ⁺, D, I', b') = TD([θ', ξ, θ⁺], D, I', b'). Sei nun θ⁺ ∈ PAR. Dann
ist [θ, ξ, θ⁺] = θ⁺ = [θ', ξ, θ⁺] und damit gilt mit TT(θ⁺) = {θ⁺}, bΓTT(θ⁺) = b'ΓTT(θ⁺) und
mit Theorem 5-2-(ii): TD([θ, ξ, θ⁺], D, I, b) = TD(θ⁺, D, I, b) = b(θ⁺) = b'(θ⁺) = TD(θ⁺,
D, I', b') = TD([θ', ξ, θ⁺], D, I', b'). Sei nun θ⁺ ∈ VAR. Dann ist θ⁺ = ξ. Dann ist [θ, ξ, θ⁺]
= θ und [θ', ξ, θ⁺] = θ'. Damit ist dann nach Annahme TD([θ, ξ, θ⁺], D, I, b) = TD(θ, D,
I, b) = TD(θ', D, I', b') = TD([θ', ξ, θ⁺], D, I', b').

Gelte die Behauptung nun fur θ⁺₀, ., θ⁺_r-1 ∈ TERM und sei φ ∈ FUNK, wobei φ r-
stellig, und sei θ⁺ = ^rφ(θ⁺o, ., θ⁺r₄)^π ∈ FTERM, wobei FV(^rφ(θ⁺o, ., θVι)^π) ⊆ {ξ},
IΓTA(^rφ(θ⁺o, ., θ⁺r-ι)^π) = I^,ΓTA(^rφ(θ⁺o, ., θ⁺r-ι)^π) und bΓTT(^rφ(θ⁺o, ., θ⁺r-ι)^π) =
bTTΓ(^rφ(θ⁺o, ., θ⁺r-ι)^π). Dann gilt mit FV(^rφ(θ⁺o, ., θ⁺r-ι)^π) = ∪{FV(θ⁺i) | i < r},
∪{TA(θ⁺i) | i < r} ⊆ TA(^rφ(θ⁺o, ., θ⁺r-ι)^π) und ∪{TT(θ⁺i) | i < r} ⊆ TΓ(^rφ(θ⁺o, .,
θ⁺r-ι)^π) fur alle i < r ebenfalls: FV(θ⁺i) ⊆ {ξ}, I ΓTA(θ⁺i) = I 'ΓTA(θ⁺i) und b ΓTT(θ⁺i) =
b'ΓTT(θ⁺i). Mit I.V. gilt somit fur alle i < r: TD([θ, ξ, θ⁺i], D, I, b) = TD([θ', ξ, θ⁺i], D, I',
b'). Sodann gilt mit φ ∈ TA(^rφ(θ⁺₀, ., θ⁺_r-1)^^l) ∩ FUNK nach Annahme auch I(φ) =
I'(φ). Damit gilt mit Theorem 5-2-(iii) insgesamt:

TD([θ, ξ, ^rφ(θ⁺Q, ., θ⁺r.ιΓ], D, I, b)

TD(^rφ([θ, ξ, θ⁺o], ., [θ, ξ, θ⁺r-ι])^¹, D, I, b)

I(φ)(<TD([θ, ξ, θ⁺o], D, I, b), ., TD([θ, ξ, θ⁺r-ι], D, I, b)>)

I'(φ)(<TD([θ', ξ, θ⁺o], D, I', b'), ., TD([θ', ξ, θ⁺r-ι], D, I, b')>)

TD(^rφ([θ^l, ξ, θ⁺Q], ., [θ', ξ, θ⁺r.ι]Γ, D, I', b')

TD([θ', ξ, ^rφ(θ⁺Q, ., θ⁺r.ιΓ], D, I', b').

Zu (ii): Der Beweis wird durch Induktion uber den Formelgrad gefuhrt. Gelte dazu das
Theorem fur alle Α ∈ FORM mit FGRAD(Α) < k. Seien nun (D, I), (D, I') Modelle, b,
b' Belegungen fur D, ξ ∈ VAR, θ, θ' ∈ GTERM und TD(θ, D, I, b) = TD(θ', D, I', b')
und sei Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ}, I ΓTA(Δ) = I ^,ΓTA(Δ) und b ΓTT(Δ) = b ^,ΓTT(Δ),
und sei FGRAD(Δ) = k. Sei FGRAD(Δ) = Q, also Δ ∈ AFORM. Dann gibt es θ⁺Q, ., θ⁺r-1

<<   <   191   192   193   194   195   196   197   >   >>