Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 191

a)   Dom(ft*) = Dom(ft')+k,

b)    ft*[^Dom(ft') = ft'

c)   VAN(ft*) ⊆ VAN(ft'),

d) Fur alle i < k-1: K(ft*fDom(ft')+i+1) = ^rΛζi+1.Λζk.1[<θ'o, ., θ'i>, <ζo, ., ζi>, [θo,
ξo, Δ]]^^, und

e)     K(ft*) = [<θ'o, ., θ'_fc-ι>, <ζo, ., ζk-1>, [θo, ξo, Δ]].

Dann ergibt sich mit a) wegen Dom(ft') = Dom(ft)+1: Dom(ft*) = Dom(ft)+k+1. Sodann
ergibt sich mit b) wegen ft'ΓDom(ft) = ft auch ft*ΓDom(ft) = ft. Mit c) ergibt sich wegen
VAN(ft') ⊆ VAN(ft), dass VAN(ft*) ⊆ VAN(ft). Damit gilt bereits, dass ft* ∈
RGS∖{0} und dass die Klauseln (i) bis (iii) fur ft* gelten. Aus d) ergibt sich sodann mit ζ_i
= ξi+1 und θ'i = θi+1:

Fur alle i < k-1: K(ft*fDom(ft')+i+1) = ^rΛξi₊2 ... Λξk[<θ₁, ., θi+1>, <ξι, ., ξ+ι>, [θo, ξo,
∆]Γ.

Mit Dom(ft') = Dom(ft)+1 gilt damit:

f) Fur alle i < k-1: K(ft*fDom(ft)+i+1+1) = ^rΛξi+₂ . Λξ_fc[<θ₁, ., θi+1>, <ξ1, ., ξi+1>, [θo,
ξo, Δ]Γ.

Damit gilt:

g) Fur alle i mit o < i < k: K(ft*[^Dom(ft)+i+1) = ^rΛξi₊1 . Λξk[<θ1, ., θi>, <ξ_b ., ξi>, [θo,
ξo, Δ]Γ.

Sodann gilt:

h) Fur alle i mit o < i < k+1: [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]] = [<θo, ., θi>, <ξo, ., ξi>,
Δ].

h) kann mittels Induktion uber i gezeigt werden. Es gilt namlich zunachst mit Theorem
1-28-(ii), dass [θ1, ξ1, [θo, ξo, Δ]] = [<θo, θ1>, <ξo, ξ1>, Δ]. Gelte nun fur i: Wenn o < i < k+1,
dann [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]] = [<θo, ., θi>, <ξo, ., ξi>, Δ]. Sei nun o < i+1 <
k+1. Dann ist i = o oder o < i. Fur i = o ergibt sich die Behauptung wie fur die Indukti-
onsbasis. Sei nun o < i. Dann ergibt sich zunachst wieder mit Theorem 1-28-(ii): [<θ1, .,
θi+1>, <ξ1, ., ξi+1>, [θo, ξo, Δ]] = [θi+1, ξi+1, [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]]]. Mit I.V. gilt
dann [θi+1, ξi+1, [<θ1, ., θi>, <ξ1, ., ξi>, [θo, ξo, Δ]]] = [θi+1, ξi+1, [<θo, ., θi>, <ξo, ., ξi>, Δ]]
und wiederum mit Theorem 1-28-(ii): [θi+1, ξi+1, [<θo, ., θi>, <ξo, ., ξi>, Δ]] = [<θo, .,

<<   164   165   166   167   168   169   170   >>

More intriguing information