Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

192   4 Theoreme zur deduktiven Konsequenzschaft

θi+ι>, <ξo, ., ξi+ι>, Δ] und damit insgesamt: [<θι, ..., θi+ι>, <ξι, ..., ξ_i+1), [θo, ξo, Δ]] = [<θo,
., θi+ι>, <ξo, ., ξi+ι>, Δ]. Also gilt h).

Sodann gilt mit Dom(S') = Dom(S)+1 und K(S*ΓDom(S')) = K(S') = ^rΛξ₁ ... Λξ_k[θ₀,
ξ₀, Δ]^^l, dass K(S*ΓDom(S)+0+1) = ^rΛξ₁ .. Λξ_k[θ₀, ξ₀, Δ]^^l. Mit g) und h) gilt dann ins-
gesamt Klausel (iv):

Fur alle i < k: K(S*fDom(S)+i+1) = ^rΛξ,_w . Λξ_k[<θo, ., θ.,), <ξo, ., ξ>, ΔJ¹.

Zuletzt gilt mit e), h) und θ'i = θi+1 und ζi = ξi+1:

K(S*) = [<θ'o, ., θ'k-i>, <ζo, ., ζk-i>, [θo, ξo, Δ]]

[<θ1, ., θk>, <ξ1, ., ξk>, [θo, ξo, Δ]]

[<θo, ., θk>, <ξo, ., ξk>, Δ]

und damit Klausel (v), womit insgesamt das Theorem fur k+1 gilt. ■

Theorem 4-13. Induktionsbasis fur Theorem 4-14

Wenn S, S' ∈ RGS∖{0} und VANS(S') = 0, dann gibt es ein S* ∈ RGS∖{0}, so dass

(i)   K(S), K(S') ∈ VER(S*) und

(ii)   VAN(S*) ⊆ VAN(S).

Beweis: Seien S, S ∈ RGS∖{0} und sei VANS(S') = 0. Wenn K(S) = K(S'), konnen so-
wohl S als auch S' fur S* gewahlt werden. Sei nun K(S) ≠ K(S'). Dann lassen sich mit
PAR ∩ TTSEQ(S) ∩ TTSEQ(S') = 0 und PAR ∩ TTSEQ(S) ∩ TTSEQ(S') ≠ 0 zwei
Falle unterscheiden.

Erster Fall: Sei PAR ∩ TTSEQ(S) ∩ TTSEQ(S') = 0. Nun gibt es ein α ∈
KONST∖(TTSEQ(S) ∪ TTSEQ(S')). Dann gibt es mit Theorem 4-4 ein S⁺ ∈ RGS∖{0},
so dass VER(S) ∪ VER(S') ⊆ VER(S⁺) und VAN(S⁺) = VAN(S) ∪ {^rα = α^^l} ∪
VAN(S'). Nun ist mit Theorem 2-82 K(S) ∈ VER(S) und K(S') ∈ VER(S') und damit
sind dann K(S), K(S') ∈ VER(S⁺). Sodann gibt es mit Theorem 4-7 S* ∈ RGS∖{0}, so
dass VAN(S*) ⊆ VAN(S⁺)∖{ ^rα = α^^l} = (VAN(S) ∪ {^rα = α^^l} ∪ VAN(S'))∖{ ^rα = α^^l}
⊆ VAN(S) ∪ VAN(S') und K(S), K(S') ∈ VER(S*), womit S* das gesuchte RGS-
Element ist.

Zweiter Fall: Sei nun PAR ∩ TTSEQ(S) ∩ TTSEQ(S') ≠ 0. Dann kommen in S' k
paarweise verschiedene Parameter fur ein k ∈ N\{o} vor. Sei nun {βo, ., βk-1} = PAR ∩

<<   165   166   167   168   169   170   171   >>

More intriguing information