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(Δ) ⊆ {ξ0, ., ξk-1}, und X H [<θ0, .,
θk-ι>, <ξo, ., ξk-ι>, Δ] und fur alle i < k: X H ^. = θ7, 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 [θ⅛, ξ⅛, [<θι, ., θ⅛4>, <ξι, ., ξ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>, Δ]. ■
More intriguing information
1. Spectral calibration of exponential Lévy Models [1]2. Quelles politiques de développement durable au Mali et à Madagascar ?
3. Antidote Stocking at Hospitals in North Palestine
4. ANTI-COMPETITIVE FINANCIAL CONTRACTING: THE DESIGN OF FINANCIAL CLAIMS.
5. The name is absent
6. The name is absent
7. The Challenge of Urban Regeneration in Deprived European Neighbourhoods - a Partnership Approach
8. LABOR POLICY AND THE OVER-ALL ECONOMY
9. The name is absent
10. The name is absent