Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

208   4 Theoreme zur deduktiven Konsequenzschaft

Sodann ist mit c) [α, ξ, Δ] = K(F) = [α, β, K(F*)]. Da nach Eingangsannahme und mit
a) gilt: α ∉ TT(Δ) ∪ TT(K(F*) ist dann mit Theorem 1-23 K(F*) = [β, ξ, Δ]. Dann ist β
∉ TT(Δ), denn sonst wurde wegen [α, ξ, Δ] = K(F) im Gegensatz zur Wahl von β gelten,
dass β ∈ TT(K(F)) ⊆ TTSEQ(F). Damit gilt dann insgesamt, dass F* ∪ {(Dom(F*),
^rAlso ΛξΔ^^l)} ∈ UEF(F*) ⊆ RGS∖{0}. Damit gilt mit Theorem 3-26-(v) VAN(F* ∪
{(Dom(F*), rʌlso ΛξΔ^^l)}) ⊆ VAN(F*) = VAN(F) ⊆ X und Theorem 3-12, dass X H
rΛξΔ^π. ■

Theorem 4-25. Mehrfache IB

Wenn k ∈ N∖{0}, {θo, ., θk-ι}, {θ'o, ., θ'k-ι} ⊆ GTERM, {ξo, ., ξ_k-ι} ⊆ VAR, wobei fur
alle i, j ∈ k mit i ≠ j auch ξ_i ≠ ξ_j∙, Δ ∈ FORM, wobei FV(Δ) ⊆ {ξ₀, ., ξ_k-1}, und X H [<θ₀, .,
θk-ι>, <ξo, ., ξk-ι>, Δ] und fur alle i < k: X H ^. = θ₇, dann X H [<θ'o, ., θ'k-ι>, <ξo, ., ξk-ι>,
Δ].

Beweis: Durch Induktion uber k. Fur k = 1 ergibt sich die Behauptung mit Theorem
4-18-(xviii). Gelte die Behauptung nun fur k und sei {θo, ., θk}, {θ'o, ., θ'k} ⊆
GTERM, {ξo, ., ξk} ⊆ VAR, wobei fur alle i, j ∈ k+1 mit i ≠ j auch ξi ≠ ξj, Δ ∈ FORM,
wobei FV(Δ) ⊆ {ξo, ., ξ_fc}, und X H [<θo, ., θ_fc>, <ξo, ., ξ_fc>, Δ] und fur alle i < k+1: X
H rθi = θ'ɔ.

Dann gilt mit Theorem 1-28-(ii), dass [<θo, ., θk>, <ξo, ., ξk>, Δ] = [θk, ξk, [<θ1, ., θk-1>,
<ξι, ., ξk-ι>, Δ]] und damit dass X H [θ⅛, ξ⅛, [<θι, ., θ⅛₄>, <ξι, ., ξk-ι>, Δ]], wobei mit
FV(Δ) ⊆ {ξo, ., ξ_fc} gilt: FV([<θι, ., θk-ι>, <ξι, ., ξk-ι>, Δ]) ⊆ {ξ_fc}. Dann gilt mit X H
rθ_fc = θ? und Theorem 4-18-(xviii), dass X H [θ'k, ξk [<θo, ., θk-ι>, <ξo, ., ξk-ι>, Δ]] und
damit wieder mit Theorem 1-28-(ii), dass X H [<θ_o, ., θ_k-1, θ'_k>, <ξ_o, ., ξ_k-1, ξ_k>, Δ]. Dann
gilt mit Theorem 1-29-(ii): [<θo, ., θk-1, θ'k>, <ξo, ., ξk-1, ξk>, Δ] = [<θo, ., θk-1>, <ξo, .,
ξk-ι>, [θ'k, ξ_k, Δ]] und damit X H [<θo, ., θ_k4>, <ξo, ., ξk-ι>, [θ'_k, ξ_k, Δ]], wobei mit FV(Δ)
⊆ {ξo, ., ξk} gilt: FV([θ'k, ξk, Δ]) ⊆ {ξo, ., ξk-ι}. Damit gilt dann nach I.V., dass X H
[<θ'o, ., θ'k-ι>, <ξo, ., ξk-ι>, [θ'k, ξk, Δ]] und damit wiederum mit Theorem 1-29-(ii): X H
[<θ'o, ., θ'k>, <ξo, ., ξk>, Δ]. ■

<<   181   182   183   184   185   186   187   >>

More intriguing information